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