Bob is blue. Bob is green. Bob is round. Charlie is blue. Charlie is green. Charlie is young. Dave is blue. Dave is cold. Dave is green. Dave is kind. If Charlie is round and Charlie is blue then Charlie is cold. Kind people are blue. If Dave is kind then Dave is green. All green, nice people are round. All green people are cold. If Charlie is cold and Charlie is young then Charlie is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
If Charlie is round and Charlie is blue then Charlie is cold.
((("Charlie" "is" "round" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "cold" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Dave is kind then Dave is green.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "green" "+"))
All green, nice people are round.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is cold and Charlie is young then Charlie is nice.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "nice" "+"))
Dave is green.
True
1
proof
[(triple9 OR ((triple10) -> rule3))]
("Dave" "is" "green" "+")
triple9
((triple10) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Charlie is not young.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "young" "-")
triple6
Charlie is cold.
True
2
proof
[(((triple5) -> rule5))]
("Charlie" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple5) -> rule5))]
("Charlie" "is" "cold" "-")
((triple5) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
True
4
proof
[(((((triple5) -> rule5) triple6) -> rule6))]
("Charlie" "is" "nice" "+")
((((triple5) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not nice.
False
4
inv-proof
[(((((triple5) -> rule5) triple6) -> rule6))]
("Charlie" "is" "nice" "-")
((((triple5) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is round.
True
6
proof
[(((triple5 ((((triple5) -> rule5) triple6) -> rule6)) -> rule4))]
("Charlie" "is" "round" "+")
((triple5 ((((triple5) -> (rule5 % int3)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not round.
False
6
inv-proof
[(((triple5 ((((triple5) -> rule5) triple6) -> rule6)) -> rule4))]
("Charlie" "is" "round" "-")
((triple5 ((((triple5) -> (rule5 % int3)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Bob is round.[(triple3)] Charlie is blue.[(triple4)] Charlie is green.[(triple5)] Charlie is young.[(triple6)] Dave is blue.[(triple7 OR ((triple10) -> rule2))] Dave is cold.[(triple8 OR ((triple9) -> rule5) OR ((((triple10) -> rule3)) -> rule5))] Dave is green.[(triple9 OR ((triple10) -> rule3))] Dave is kind.[(triple10)] @1: Bob is cold.[(((triple2) -> rule5))] Charlie is cold.[(((triple5) -> rule5))] @2: Charlie is nice.[(((((triple5) -> rule5) triple6) -> rule6))] @3: Charlie is round.[(((triple5 ((((triple5) -> rule5) triple6) -> rule6)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
((triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple8
((triple9) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple9
((triple10) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple5) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple5 ((((triple5) -> (rule5 % int3)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3