Bob is blue. Bob is cold. Bob is white. Charlie is big. Charlie is kind. Charlie is nice. Charlie is round. If someone is cold then they are white. If Bob is blue and Bob is kind then Bob is white. If someone is cold then they are round. White, kind people are blue. Cold people are round. Kind people are cold.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If someone is cold then they are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Bob is blue and Bob is kind then Bob is white.
((("Bob" "is" "blue" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "white" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
White, kind people are blue.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Charlie is round.
True
1
proof
[(triple7 OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6)) -> rule5))]
("Charlie" "is" "round" "+")
triple7
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not round.
False
1
inv-proof
[(triple7 OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6)) -> rule5))]
("Charlie" "is" "round" "-")
triple7
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Bob is round.
True
2
proof
[(((triple2) -> rule3) OR ((triple2) -> rule5))]
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple5) -> rule6))]
("Charlie" "is" "cold" "-")
((triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
True
3
proof
[(((((triple5) -> rule6)) -> rule1))]
("Charlie" "is" "white" "+")
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule1))]
("Charlie" "is" "white" "-")
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
True
5
proof
[(((((((triple5) -> rule6)) -> rule1) triple5) -> rule4))]
("Charlie" "is" "blue" "+")
((((((triple5) -> (rule6 % int3))) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((((((triple5) -> rule6)) -> rule1) triple5) -> rule4))]
("Charlie" "is" "blue" "-")
((((((triple5) -> (rule6 % int3))) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is white.[(triple3 OR ((triple2) -> rule1))] Charlie is big.[(triple4)] Charlie is kind.[(triple5)] Charlie is nice.[(triple6)] Charlie is round.[(triple7 OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6)) -> rule5))] @1: Bob is round.[(((triple2) -> rule3) OR ((triple2) -> rule5))] Charlie is cold.[(((triple5) -> rule6))] @2: Charlie is white.[(((((triple5) -> rule6)) -> rule1))] @3: Charlie is blue.[(((((((triple5) -> rule6)) -> rule1) triple5) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple5) -> (rule6 % int3))) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3