Bob is green. Bob is nice. Bob is quiet. Erin is quiet. Erin is red. Gary is big. Gary is red. If Bob is red then Bob is not nice. If someone is cold and quiet then they are rough. Nice people are green. All big, red people are green. If Erin is quiet then Erin is cold. If someone is red and rough then they are big.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is red.
("Gary" "is" "red" "+")
If Bob is red then Bob is not nice.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "nice" "-"))
If someone is cold and quiet then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All big, red people are green.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If Erin is quiet then Erin is cold.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "cold" "+"))
If someone is red and rough then they are big.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Bob is green.
True
1
proof
[(triple1 OR ((triple2) -> rule3))]
("Bob" "is" "green" "+")
triple1
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Erin is cold.
True
2
proof
[(((triple4) -> rule5))]
("Erin" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is not green.
False
3
inv-proof
[(((triple6 triple7) -> rule4))]
("Gary" "is" "green" "-")
((triple6 triple7) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is rough.
True
4
proof
[(((((triple4) -> rule5) triple4) -> rule2))]
("Erin" "is" "rough" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((((triple4) -> rule5) triple4) -> rule2))]
("Erin" "is" "rough" "-")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
True
6
proof
[(((triple5 ((((triple4) -> rule5) triple4) -> rule2)) -> rule6))]
("Erin" "is" "big" "+")
((triple5 ((((triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not big.
False
6
inv-proof
[(((triple5 ((((triple4) -> rule5) triple4) -> rule2)) -> rule6))]
("Erin" "is" "big" "-")
((triple5 ((((triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "big" "+")
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1 OR ((triple2) -> rule3))] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Erin is quiet.[(triple4)] Erin is red.[(triple5)] Gary is big.[(triple6)] Gary is red.[(triple7)] @1: Erin is cold.[(((triple4) -> rule5))] Gary is green.[(((triple6 triple7) -> rule4))] @2: Erin is rough.[(((((triple4) -> rule5) triple4) -> rule2))] @3: Erin is big.[(((triple5 ((((triple4) -> rule5) triple4) -> rule2)) -> rule6))] @4: Erin is green.[(((((triple5 ((((triple4) -> rule5) triple4) -> rule2)) -> rule6) triple5) -> rule4))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6 triple7) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple5 ((((triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((triple5 ((((triple4) -> (rule5 % int4)) triple4) -> (rule2 % int3))) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4