Charlie is round. Dave is red. Dave is round. Erin is kind. Erin is red. Erin is smart. Erin is young. Gary is red. Gary is round. Gary is young. Round, red things are smart. All nice, red things are big. All kind things are nice. If Dave is kind and Dave is round then Dave is smart. If something is smart then it is kind. If something is big then it is young.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Round, red things are smart.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All nice, red things are big.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Dave is kind and Dave is round then Dave is smart.
((("Dave" "is" "kind" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "smart" "+"))
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Gary is red.
True
1
proof
[(triple8)]
("Gary" "is" "red" "+")
triple8
Gary is not round.
False
1
inv-proof
[(triple9)]
("Gary" "is" "round" "-")
triple9
Gary is smart.
True
3
proof
[(((triple9 triple8) -> rule1))]
("Gary" "is" "smart" "+")
((triple9 triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
3
inv-proof
[(((triple9 triple8) -> rule1))]
("Gary" "is" "smart" "-")
((triple9 triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Erin is big.
True
4
proof
[(((((triple4) -> rule3) triple5) -> rule2) OR ((((((triple6) -> rule5)) -> rule3) triple5) -> rule2))]
("Erin" "is" "big" "+")
((((triple4) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Dave is not kind.
False
4
inv-proof
[(((((triple3 triple2) -> rule1)) -> rule5))]
("Dave" "is" "kind" "-")
((((triple3 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Gary is nice.
True
5
proof
[(((((((triple9 triple8) -> rule1)) -> rule5)) -> rule3))]
("Gary" "is" "nice" "+")
((((((triple9 triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not nice.
False
5
inv-proof
[(((((((triple9 triple8) -> rule1)) -> rule5)) -> rule3))]
("Gary" "is" "nice" "-")
((((((triple9 triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is big.
True
7
proof
[(((((((((triple9 triple8) -> rule1)) -> rule5)) -> rule3) triple8) -> rule2))]
("Gary" "is" "big" "+")
((((((((triple9 triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not big.
False
7
inv-proof
[(((((((((triple9 triple8) -> rule1)) -> rule5)) -> rule3) triple8) -> rule2))]
("Gary" "is" "big" "-")
((((((((triple9 triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Dave is young.
True
8
proof
[(((((((((((triple3 triple2) -> rule1)) -> rule5)) -> rule3) triple2) -> rule2)) -> rule6))]
("Dave" "is" "young" "+")
((((((((((triple3 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Dave is not young.
False
8
inv-proof
[(((((((((((triple3 triple2) -> rule1)) -> rule5)) -> rule3) triple2) -> rule2)) -> rule6))]
("Dave" "is" "young" "-")
((((((((((triple3 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is nice.
Unknown
rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not kind.
Unknown
inv-rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Charlie is round.[(triple1)] Dave is red.[(triple2)] Dave is round.[(triple3)] Erin is kind.[(triple4 OR ((triple6) -> rule5))] Erin is red.[(triple5)] Erin is smart.[(triple6)] Erin is young.[(triple7 OR ((((((triple4) -> rule3) triple5) -> rule2)) -> rule6) OR ((((((((triple6) -> rule5)) -> rule3) triple5) -> rule2)) -> rule6))] Gary is red.[(triple8)] Gary is round.[(triple9)] Gary is young.[(triple10 OR ((((((((((triple9 triple8) -> rule1)) -> rule5)) -> rule3) triple8) -> rule2)) -> rule6))] @1: Dave is smart.[(((triple3 triple2) -> rule1))] Erin is nice.[(((triple4) -> rule3) OR ((((triple6) -> rule5)) -> rule3))] Gary is smart.[(((triple9 triple8) -> rule1))] @2: Dave is kind.[(((((triple3 triple2) -> rule1)) -> rule5))] Erin is big.[(((((triple4) -> rule3) triple5) -> rule2) OR ((((((triple6) -> rule5)) -> rule3) triple5) -> rule2))] Gary is kind.[(((((triple9 triple8) -> rule1)) -> rule5))] @3: Dave is nice.[(((((((triple3 triple2) -> rule1)) -> rule5)) -> rule3))] Gary is nice.[(((((((triple9 triple8) -> rule1)) -> rule5)) -> rule3))] @4: Dave is big.[(((((((((triple3 triple2) -> rule1)) -> rule5)) -> rule3) triple2) -> rule2))] Gary is big.[(((((((((triple9 triple8) -> rule1)) -> rule5)) -> rule3) triple8) -> rule2))] @5: Dave is young.[(((((((((((triple3 triple2) -> rule1)) -> rule5)) -> rule3) triple2) -> rule2)) -> rule6))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple6) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
((((((triple4) -> (rule3 % int3)) triple5) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((((((((triple6) -> (rule5 % int4))) -> (rule3 % int3)) triple5) -> (rule2 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((((((((((triple9 triple8) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple8) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Dave is smart.
("Dave" "is" "smart" "+")
((triple3 triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple9 triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple3 triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple4) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((triple9 triple8) -> (rule1 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple3 triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple9 triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((((triple3 triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
((((((((triple9 triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
((((((((((triple3 triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5