Anne is green. Anne is kind. Anne is quiet. Anne is red. Anne is round. Charlie is kind. Charlie is quiet. Charlie is round. Fiona is kind. Fiona is quiet. Fiona is red. Fiona is round. Harry is big. Harry is kind. Harry is red. All smart, red things are quiet. Quiet things are red. Red things are kind. If Charlie is red then Charlie is quiet. If Fiona is round and Fiona is kind then Fiona is red. If something is big and red then it is green. If something is smart and quiet then it is kind. If something is round then it is red.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
All smart, red things are quiet.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Charlie is red then Charlie is quiet.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "quiet" "+"))
If Fiona is round and Fiona is kind then Fiona is red.
((("Fiona" "is" "round" "+") ("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "red" "+"))
If something is big and red then it is green.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is smart and quiet then it is kind.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Anne is red.
True
1
proof
[(triple4 OR ((triple3) -> rule2) OR ((triple5) -> rule8))]
("Anne" "is" "red" "+")
triple4
((triple3) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple5) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is not round.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "round" "-")
triple8
Harry is green.
True
3
proof
[(((triple13 triple15) -> rule6))]
("Harry" "is" "green" "+")
((triple13 triple15) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
3
inv-proof
[(((triple13 triple15) -> rule6))]
("Harry" "is" "green" "-")
((triple13 triple15) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "green" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is green.[(triple1)] Anne is kind.[(triple2 OR ((triple4) -> rule3) OR ((((triple3) -> rule2)) -> rule3) OR ((((triple5) -> rule8)) -> rule3))] Anne is quiet.[(triple3)] Anne is red.[(triple4 OR ((triple3) -> rule2) OR ((triple5) -> rule8))] Anne is round.[(triple5)] Charlie is kind.[(triple6 OR ((((triple7) -> rule2)) -> rule3) OR ((((triple8) -> rule8)) -> rule3))] Charlie is quiet.[(triple7 OR ((((triple8) -> rule8)) -> rule4))] Charlie is round.[(triple8)] Fiona is kind.[(triple9 OR ((triple11) -> rule3) OR ((((triple10) -> rule2)) -> rule3) OR ((((triple12) -> rule8)) -> rule3))] Fiona is quiet.[(triple10)] Fiona is red.[(triple11 OR ((triple10) -> rule2) OR ((triple12) -> rule8) OR ((triple12 triple9) -> rule5))] Fiona is round.[(triple12)] Harry is big.[(triple13)] Harry is kind.[(triple14 OR ((triple15) -> rule3))] Harry is red.[(triple15)] @1: Charlie is red.[(((triple7) -> rule2) OR ((triple8) -> rule8))] Harry is green.[(((triple13 triple15) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple4) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple3) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple5) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple8) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
((((triple8) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
((triple11) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple12) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple11
((triple10) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple12) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple12 triple9) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((triple15) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple15
Charlie is red.
("Charlie" "is" "red" "+")
((triple7) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple8) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple13 triple15) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1