Bob is blue. Bob is cold. Bob is kind. Bob is rough. Bob is smart. Bob is white. Dave is rough. Dave is smart. Erin is blue. Erin is white. Gary is blue. Gary is cold. Gary is kind. Gary is quiet. Gary is smart. Gary is white. Cold things are blue. If something is white and blue then it is rough. If something is rough and white then it is cold. All cold things are kind. If Gary is cold then Gary is rough. If Gary is rough then Gary is smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is white and blue then it is rough.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is rough and white then it is cold.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If Gary is cold then Gary is rough.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is rough then Gary is smart.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "smart" "+"))
Erin is white.
True
1
proof
[(triple10)]
("Erin" "is" "white" "+")
triple10
Bob is not rough.
False
1
inv-proof
[(triple4 OR ((triple6 triple1) -> rule2) OR ((triple6 ((triple2) -> rule1)) -> rule2))]
("Bob" "is" "rough" "-")
triple4
((triple6 triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Gary is rough.
True
2
proof
[(((triple12) -> rule5) OR ((triple16 triple11) -> rule2) OR ((triple16 ((triple12) -> rule1)) -> rule2))]
("Gary" "is" "rough" "+")
((triple12) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple16 triple11) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple16 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((triple10 triple9) -> rule2))]
("Erin" "is" "rough" "-")
((triple10 triple9) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
True
5
proof
[(((((triple10 triple9) -> rule2) triple10) -> rule3))]
("Erin" "is" "cold" "+")
((((triple10 triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not cold.
False
5
inv-proof
[(((((triple10 triple9) -> rule2) triple10) -> rule3))]
("Erin" "is" "cold" "-")
((((triple10 triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
True
6
proof
[(((((((triple10 triple9) -> rule2) triple10) -> rule3)) -> rule4))]
("Erin" "is" "kind" "+")
((((((triple10 triple9) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not kind.
False
6
inv-proof
[(((((((triple10 triple9) -> rule2) triple10) -> rule3)) -> rule4))]
("Erin" "is" "kind" "-")
((((((triple10 triple9) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is kind.
Unknown
rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Dave" "is" "kind" "+")
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule1) OR ((((triple4 triple6) -> rule3)) -> rule1))] Bob is cold.[(triple2 OR ((triple4 triple6) -> rule3) OR ((((triple6 triple1) -> rule2) triple6) -> rule3))] Bob is kind.[(triple3 OR ((triple2) -> rule4) OR ((((triple4 triple6) -> rule3)) -> rule4) OR ((((((triple6 triple1) -> rule2) triple6) -> rule3)) -> rule4))] Bob is rough.[(triple4 OR ((triple6 triple1) -> rule2) OR ((triple6 ((triple2) -> rule1)) -> rule2))] Bob is smart.[(triple5)] Bob is white.[(triple6)] Dave is rough.[(triple7)] Dave is smart.[(triple8)] Erin is blue.[(triple9)] Erin is white.[(triple10)] Gary is blue.[(triple11 OR ((triple12) -> rule1))] Gary is cold.[(triple12 OR ((((triple16 triple11) -> rule2) triple16) -> rule3))] Gary is kind.[(triple13 OR ((triple12) -> rule4) OR ((((((triple16 triple11) -> rule2) triple16) -> rule3)) -> rule4))] Gary is quiet.[(triple14)] Gary is smart.[(triple15 OR ((((triple12) -> rule5)) -> rule6) OR ((((triple16 triple11) -> rule2)) -> rule6) OR ((((triple16 ((triple12) -> rule1)) -> rule2)) -> rule6))] Gary is white.[(triple16)] @1: Erin is rough.[(((triple10 triple9) -> rule2))] Gary is rough.[(((triple12) -> rule5) OR ((triple16 triple11) -> rule2) OR ((triple16 ((triple12) -> rule1)) -> rule2))] @2: Erin is cold.[(((((triple10 triple9) -> rule2) triple10) -> rule3))] @3: Erin is kind.[(((((((triple10 triple9) -> rule2) triple10) -> rule3)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple4 triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple6 triple1) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple4 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple6 triple1) -> (rule2 % int3)) triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple6 triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple6 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Gary is blue.
("Gary" "is" "blue" "+")
triple11
((triple12) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple12
((((triple16 triple11) -> (rule2 % int2)) triple16) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple13
((triple12) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((((triple16 triple11) -> (rule2 % int3)) triple16) -> (rule3 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
((((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple16 triple11) -> (rule2 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple16 ((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple16
Erin is rough.
("Erin" "is" "rough" "+")
((triple10 triple9) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple12) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple16 triple11) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple16 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple10 triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple10 triple9) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3