Charlie is big. Charlie is green. Charlie is kind. Charlie is not quiet. Charlie is red. Charlie is young. Dave is big. Dave is green. Dave is kind. Dave is quiet. Dave is red. Dave is not round. Dave is young. Fiona is not round. Harry is quiet. Green, big things are young. If Dave is not kind then Dave is big. If Dave is young then Dave is quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is young.
("Dave" "is" "young" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Green, big things are young.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Dave is not kind then Dave is big.
((("Dave" "is" "kind" "~")) -> ("Dave" "is" "big" "+"))
If Dave is young then Dave is quiet.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "quiet" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "young" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2)] Charlie is kind.[(triple3)] Charlie is not quiet.[(triple4)] Charlie is red.[(triple5)] Charlie is young.[(triple6 OR ((triple2 triple1) -> rule1))] Dave is big.[(triple7)] Dave is green.[(triple8)] Dave is kind.[(triple9)] Dave is not round.[(triple12)] Dave is quiet.[(triple10 OR ((triple13) -> rule3) OR ((((triple8 triple7) -> rule1)) -> rule3))] Dave is red.[(triple11)] Dave is young.[(triple13 OR ((triple8 triple7) -> rule1))] Fiona is not round.[(triple14)] Harry is quiet.[(triple15)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple2 triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is not round.
("Dave" "is" "round" "-")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
((triple13) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple8 triple7) -> (rule1 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple13
((triple8 triple7) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is not round.
("Fiona" "is" "round" "-")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15