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