Anne is red. Bob is cold. Charlie is white. Erin is smart. All smart, big people are rough. If Charlie is smart then Charlie is white. Cold people are big. If someone is big then they are smart. All red, smart people are kind. If someone is red then they are cold. If someone is rough and cold then they are smart. If Anne is rough then Anne is white.
Anne is red.
("Anne" "is" "red" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All smart, big people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is smart then Charlie is white.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "white" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All red, smart people are kind.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and cold then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If Anne is rough then Anne is white.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "white" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Charlie is not white.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "white" "-")
triple3
Anne is cold.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "big" "-")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Anne is smart.
True
4
proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule4))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not smart.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule4))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "kind" "-")
Charlie is smart.
Unknown
rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is red.[(triple1)] Bob is cold.[(triple2)] Charlie is white.[(triple3)] Erin is smart.[(triple4)] @1: Anne is cold.[(((triple1) -> rule6))] Bob is big.[(((triple2) -> rule3))] @2: Anne is big.[(((((triple1) -> rule6)) -> rule3))] Bob is smart.[(((((triple2) -> rule3)) -> rule4))] @3: Anne is smart.[(((((((triple1) -> rule6)) -> rule3)) -> rule4))] Bob is rough.[(((((((triple2) -> rule3)) -> rule4) ((triple2) -> rule3)) -> rule1))] @4: Anne is kind.[(((triple1 ((((((triple1) -> rule6)) -> rule3)) -> rule4)) -> rule5))] Anne is rough.[(((((((((triple1) -> rule6)) -> rule3)) -> rule4) ((((triple1) -> rule6)) -> rule3)) -> rule1))] @5: Anne is white.[(((((((((((triple1) -> rule6)) -> rule3)) -> rule4) ((((triple1) -> rule6)) -> rule3)) -> rule1)) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((((((triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((((triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((((((((triple1) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5