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