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