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