Anne is cold. Bob is big. Bob is blue. Bob is cold. Bob is nice. Charlie is kind. Erin is big. Erin is blue. Erin is nice. Erin is round. Round, nice things are kind. If something is kind then it is rough. All round things are big. If Anne is kind and Anne is rough then Anne is round. If something is cold then it is round. If something is round and cold then it is big.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Round, nice things are kind.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Anne is kind and Anne is rough then Anne is round.
((("Anne" "is" "kind" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "round" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is round and cold then it is big.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Erin is blue.
True
1
proof
[(triple8)]
("Erin" "is" "blue" "+")
triple8
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Erin is kind.
True
3
proof
[(((triple10 triple9) -> rule1))]
("Erin" "is" "kind" "+")
((triple10 triple9) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
3
inv-proof
[(((triple10 triple9) -> rule1))]
("Erin" "is" "kind" "-")
((triple10 triple9) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule3) OR ((((triple1) -> rule5) triple1) -> rule6))]
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3) OR ((((triple1) -> rule5) triple1) -> rule6))]
("Anne" "is" "big" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is rough.
True
5
proof
[(((((((triple4) -> rule5) triple5) -> rule1)) -> rule2))]
("Bob" "is" "rough" "+")
((((((triple4) -> (rule5 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((((((triple4) -> rule5) triple5) -> rule1)) -> rule2))]
("Bob" "is" "rough" "-")
((((((triple4) -> (rule5 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "big" "+")
Anne is not rough.
Unknown
inv-rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Bob is big.[(triple2 OR ((((triple4) -> rule5)) -> rule3) OR ((((triple4) -> rule5) triple4) -> rule6))] Bob is blue.[(triple3)] Bob is cold.[(triple4)] Bob is nice.[(triple5)] Charlie is kind.[(triple6)] Erin is big.[(triple7 OR ((triple10) -> rule3))] Erin is blue.[(triple8)] Erin is nice.[(triple9)] Erin is round.[(triple10)] @1: Anne is round.[(((triple1) -> rule5))] Bob is round.[(((triple4) -> rule5))] Charlie is rough.[(((triple6) -> rule2))] Erin is kind.[(((triple10 triple9) -> rule1))] @2: Anne is big.[(((((triple1) -> rule5)) -> rule3) OR ((((triple1) -> rule5) triple1) -> rule6))] Bob is kind.[(((((triple4) -> rule5) triple5) -> rule1))] Erin is rough.[(((((triple10 triple9) -> rule1)) -> rule2))] @3: Bob is rough.[(((((((triple4) -> rule5) triple5) -> rule1)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple4) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
((triple10) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple4) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple6) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple10 triple9) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple4) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple10 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple4) -> (rule5 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3