Charlie is big. Charlie is blue. Charlie is cold. Charlie is white. Dave is blue. Dave is green. Harry is big. Harry is cold. Harry is green. Harry is kind. Harry is round. Harry is white. If Dave is blue and Dave is big then Dave is kind. If Harry is kind then Harry is round. If something is green and blue then it is big. Kind things are cold. If something is round then it is big. All kind, white things are cold.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Dave is blue and Dave is big then Dave is kind.
((("Dave" "is" "blue" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
If Harry is kind then Harry is round.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "+"))
If something is green and blue then it is big.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All kind, white things are cold.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Harry is green.
True
1
proof
[(triple9)]
("Harry" "is" "green" "+")
triple9
Harry is not white.
False
1
inv-proof
[(triple12)]
("Harry" "is" "white" "-")
triple12
Dave is big.
True
3
proof
[(((triple6 triple5) -> rule3))]
("Dave" "is" "big" "+")
((triple6 triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
3
inv-proof
[(((triple6 triple5) -> rule3))]
("Dave" "is" "big" "-")
((triple6 triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
True
5
proof
[(((triple5 ((triple6 triple5) -> rule3)) -> rule1))]
("Dave" "is" "kind" "+")
((triple5 ((triple6 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not kind.
False
5
inv-proof
[(((triple5 ((triple6 triple5) -> rule3)) -> rule1))]
("Dave" "is" "kind" "-")
((triple5 ((triple6 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
True
6
proof
[(((((triple5 ((triple6 triple5) -> rule3)) -> rule1)) -> rule4))]
("Dave" "is" "cold" "+")
((((triple5 ((triple6 triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not cold.
False
6
inv-proof
[(((((triple5 ((triple6 triple5) -> rule3)) -> rule1)) -> rule4))]
("Dave" "is" "cold" "-")
((((triple5 ((triple6 triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is cold.[(triple3)] Charlie is white.[(triple4)] Dave is blue.[(triple5)] Dave is green.[(triple6)] Harry is big.[(triple7 OR ((triple11) -> rule5) OR ((((triple10) -> rule2)) -> rule5))] Harry is cold.[(triple8 OR ((triple10) -> rule4) OR ((triple10 triple12) -> rule6))] Harry is green.[(triple9)] Harry is kind.[(triple10)] Harry is round.[(triple11 OR ((triple10) -> rule2))] Harry is white.[(triple12)] @1: Dave is big.[(((triple6 triple5) -> rule3))] @2: Dave is kind.[(((triple5 ((triple6 triple5) -> rule3)) -> rule1))] @3: Dave is cold.[(((((triple5 ((triple6 triple5) -> rule3)) -> rule1)) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple11) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple10) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple10 triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
((triple10) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple12
Dave is big.
("Dave" "is" "big" "+")
((triple6 triple5) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple5 ((triple6 triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple5 ((triple6 triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3