Charlie is kind. Charlie is nice. Dave is kind. Dave is young. Gary is nice. Gary is round. Harry is round. Round people are blue. Round, nice people are kind. If someone is nice and kind then they are cold. All cold people are round. Round, blue people are young. If someone is green and cold then they are young. Blue, green people are cold. If someone is nice and young then they are green.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is round.
("Harry" "is" "round" "+")
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Round, nice people are kind.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice and kind then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Round, blue people are young.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is green and cold then they are young.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Blue, green people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and young then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Dave is young.
True
1
proof
[(triple4)]
("Dave" "is" "young" "+")
triple4
Harry is not round.
False
1
inv-proof
[(triple7)]
("Harry" "is" "round" "-")
triple7
Gary is blue.
True
2
proof
[(((triple6) -> rule1))]
("Gary" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple6) -> rule1))]
("Gary" "is" "blue" "-")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
True
5
proof
[(((triple5 ((triple6 triple5) -> rule2)) -> rule3) OR ((((triple6) -> rule1) ((triple5 ((triple6 ((triple6) -> rule1)) -> rule5)) -> rule8)) -> rule7))]
("Gary" "is" "cold" "+")
((triple5 ((triple6 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple6) -> (rule1 % int4)) ((triple5 ((triple6 ((triple6) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is not young.
False
4
inv-proof
[(((triple6 ((triple6) -> rule1)) -> rule5))]
("Gary" "is" "young" "-")
((triple6 ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is blue.
True
5
proof
[(((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1))]
("Charlie" "is" "blue" "+")
((((((triple2 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1))]
("Charlie" "is" "blue" "-")
((((((triple2 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
True
10
proof
[(((((((triple2 triple1) -> rule3)) -> rule4) ((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1)) -> rule5))]
("Charlie" "is" "young" "+")
((((((triple2 triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((((((triple2 triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is not young.
False
10
inv-proof
[(((((((triple2 triple1) -> rule3)) -> rule4) ((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1)) -> rule5))]
("Charlie" "is" "young" "-")
((((((triple2 triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((((((triple2 triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is green.
True
12
proof
[(((triple2 ((((((triple2 triple1) -> rule3)) -> rule4) ((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1)) -> rule5)) -> rule8))]
("Charlie" "is" "green" "+")
((triple2 ((((((triple2 triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple2 triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
Charlie is not green.
False
12
inv-proof
[(((triple2 ((((((triple2 triple1) -> rule3)) -> rule4) ((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1)) -> rule5)) -> rule8))]
("Charlie" "is" "green" "-")
((triple2 ((((((triple2 triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple2 triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "+")
Dave is not blue.
Unknown
inv-rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Dave" "is" "cold" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "green" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Charlie is kind.[(triple1)] Charlie is nice.[(triple2)] Dave is kind.[(triple3)] Dave is young.[(triple4)] Gary is nice.[(triple5)] Gary is round.[(triple6)] Harry is round.[(triple7)] @1: Charlie is cold.[(((triple2 triple1) -> rule3))] Gary is blue.[(((triple6) -> rule1))] Gary is kind.[(((triple6 triple5) -> rule2))] Harry is blue.[(((triple7) -> rule1))] @2: Charlie is round.[(((((triple2 triple1) -> rule3)) -> rule4))] Gary is cold.[(((triple5 ((triple6 triple5) -> rule2)) -> rule3) OR ((((triple6) -> rule1) ((triple5 ((triple6 ((triple6) -> rule1)) -> rule5)) -> rule8)) -> rule7))] Gary is young.[(((triple6 ((triple6) -> rule1)) -> rule5))] Harry is young.[(((triple7 ((triple7) -> rule1)) -> rule5))] @3: Charlie is blue.[(((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1))] Gary is green.[(((triple5 ((triple6 ((triple6) -> rule1)) -> rule5)) -> rule8))] @4: Charlie is young.[(((((((triple2 triple1) -> rule3)) -> rule4) ((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1)) -> rule5))] @5: Charlie is green.[(((triple2 ((((((triple2 triple1) -> rule3)) -> rule4) ((((((triple2 triple1) -> rule3)) -> rule4)) -> rule1)) -> rule5)) -> rule8))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2 triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6 triple5) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple5 ((triple6 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple6) -> (rule1 % int4)) ((triple5 ((triple6 ((triple6) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
((triple6 ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple2 triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((triple5 ((triple6 ((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple2 triple1) -> (rule3 % int4))) -> (rule4 % int3)) ((((((triple2 triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
((triple2 ((((((triple2 triple1) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple2 triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
int5