Charlie is not big. Charlie is not white. Dave is not cold. Dave is red. Gary is red. Gary is white. Harry is not big. Harry is blue. Harry is cold. Harry is kind. Harry is red. Harry is round. If Dave is big then Dave is kind. If someone is red and not cold then they are big. If someone is big and kind then they are not round. Blue, red people are not white. If someone is red and not round then they are blue.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is red.
("Dave" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If Dave is big then Dave is kind.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
If someone is red and not cold then they are big.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "+"))
If someone is big and kind then they are not round.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "-"))
Blue, red people are not white.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "-"))
If someone is red and not round then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "blue" "+"))
Harry is not big.
True
1
proof
[(triple7)]
("Harry" "is" "big" "-")
triple7
Charlie is white.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "white" "+")
triple2
Harry is not white.
True
3
proof
[(((triple8 triple11) -> rule4))]
("Harry" "is" "white" "-")
((triple8 triple11) -> (rule4 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Dave is not big.
False
3
inv-proof
[(((triple4 triple3) -> rule2))]
("Dave" "is" "big" "-")
((triple4 triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
True
4
proof
[(((((triple4 triple3) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple4 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((((triple4 triple3) -> rule2)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple4 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not round.
True
8
proof
[(((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "round" "-")
((((triple4 triple3) -> (rule2 % int3)) ((((triple4 triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
False
8
inv-proof
[(((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3))]
("Dave" "is" "round" "+")
((((triple4 triple3) -> (rule2 % int3)) ((((triple4 triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is blue.
True
10
proof
[(((triple4 ((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3)) -> rule5))]
("Dave" "is" "blue" "+")
((triple4 ((((triple4 triple3) -> (rule2 % int4)) ((((triple4 triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not blue.
False
10
inv-proof
[(((triple4 ((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3)) -> rule5))]
("Dave" "is" "blue" "-")
((triple4 ((((triple4 triple3) -> (rule2 % int4)) ((((triple4 triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not white.
True
12
proof
[(((((triple4 ((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3)) -> rule5) triple4) -> rule4))]
("Dave" "is" "white" "-")
((((triple4 ((((triple4 triple3) -> (rule2 % int5)) ((((triple4 triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5
Dave is white.
False
12
inv-proof
[(((((triple4 ((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3)) -> rule5) triple4) -> rule4))]
("Dave" "is" "white" "+")
((((triple4 ((((triple4 triple3) -> (rule2 % int5)) ((((triple4 triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is not big.[(triple1)] Charlie is not white.[(triple2)] Dave is not cold.[(triple3)] Dave is red.[(triple4)] Gary is red.[(triple5)] Gary is white.[(triple6)] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is kind.[(triple10)] Harry is not big.[(triple7)] Harry is red.[(triple11)] Harry is round.[(triple12)] @1: Dave is big.[(((triple4 triple3) -> rule2))] Harry is not white.[(((triple8 triple11) -> rule4))] @2: Dave is kind.[(((((triple4 triple3) -> rule2)) -> rule1))] @3: Dave is not round.[(((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3))] @4: Dave is blue.[(((triple4 ((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3)) -> rule5))] @5: Dave is not white.[(((((triple4 ((((triple4 triple3) -> rule2) ((((triple4 triple3) -> rule2)) -> rule1)) -> rule3)) -> rule5) triple4) -> rule4))]
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is not white.
("Charlie" "is" "white" "-")
triple2
Dave is not cold.
("Dave" "is" "cold" "-")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is not big.
("Harry" "is" "big" "-")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Dave is big.
("Dave" "is" "big" "+")
((triple4 triple3) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple8 triple11) -> (rule4 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple4 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
((((triple4 triple3) -> (rule2 % int3)) ((((triple4 triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((triple4 ((((triple4 triple3) -> (rule2 % int4)) ((((triple4 triple3) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not white.
("Dave" "is" "white" "-")
((((triple4 ((((triple4 triple3) -> (rule2 % int5)) ((((triple4 triple3) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5