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