Bob is young. Charlie is furry. Charlie is red. Dave is cold. Erin is nice. Erin is red. Erin is young. If something is young and red then it is round. Nice, round things are furry. If something is cold then it is nice. Furry, cold things are round. If something is cold and nice then it is white. If something is white and red then it is round. All round things are red. All round, cold things are furry. Nice, white things are red.
Bob is young.
("Bob" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is young and red then it is round.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Nice, round things are furry.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Furry, cold things are round.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is cold and nice then it is white.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is white and red then it is round.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All round, cold things are furry.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Nice, white things are red.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Erin is nice.
True
1
proof
[(triple5)]
("Erin" "is" "nice" "+")
triple5
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
Erin is round.
True
3
proof
[(((triple7 triple6) -> rule1))]
("Erin" "is" "round" "+")
((triple7 triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
3
inv-proof
[(((triple7 triple6) -> rule1))]
("Erin" "is" "round" "-")
((triple7 triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Dave is white.
True
4
proof
[(((triple4 ((triple4) -> rule3)) -> rule5))]
("Dave" "is" "white" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not white.
False
4
inv-proof
[(((triple4 ((triple4) -> rule3)) -> rule5))]
("Dave" "is" "white" "-")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
True
7
proof
[(((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9))]
("Dave" "is" "red" "+")
((((triple4) -> (rule3 % int3)) ((triple4 ((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not red.
False
7
inv-proof
[(((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9))]
("Dave" "is" "red" "-")
((((triple4) -> (rule3 % int3)) ((triple4 ((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is round.
True
12
proof
[(((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6))]
("Dave" "is" "round" "+")
((((triple4 ((triple4) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple4) -> (rule3 % int4)) ((triple4 ((triple4) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not round.
False
12
inv-proof
[(((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6))]
("Dave" "is" "round" "-")
((((triple4 ((triple4) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple4) -> (rule3 % int4)) ((triple4 ((triple4) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is furry.
True
14
proof
[(((((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6) triple4) -> rule8) OR ((((triple4) -> rule3) ((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6)) -> rule2))]
("Dave" "is" "furry" "+")
((((((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple4) -> (rule3 % int5)) ((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) triple4) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
((((triple4) -> (rule3 % int5)) ((((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple4) -> (rule3 % int5)) ((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not furry.
False
14
inv-proof
[(((((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6) triple4) -> rule8) OR ((((triple4) -> rule3) ((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6)) -> rule2))]
("Dave" "is" "furry" "-")
((((((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple4) -> (rule3 % int5)) ((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) triple4) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
((((triple4) -> (rule3 % int5)) ((((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple4) -> (rule3 % int5)) ((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "white" "+")
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not round.
Unknown
inv-rconc
[@4: Bob is round.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule6 <- rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is young.[(triple1)] Charlie is furry.[(triple2)] Charlie is red.[(triple3)] Dave is cold.[(triple4)] Erin is nice.[(triple5)] Erin is red.[(triple6)] Erin is young.[(triple7)] @1: Dave is nice.[(((triple4) -> rule3))] Erin is round.[(((triple7 triple6) -> rule1))] @2: Dave is white.[(((triple4 ((triple4) -> rule3)) -> rule5))] Erin is furry.[(((triple5 ((triple7 triple6) -> rule1)) -> rule2))] @3: Dave is red.[(((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9))] @4: Dave is round.[(((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6))] @5: Dave is furry.[(((((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6) triple4) -> rule8) OR ((((triple4) -> rule3) ((((triple4 ((triple4) -> rule3)) -> rule5) ((((triple4) -> rule3) ((triple4 ((triple4) -> rule3)) -> rule5)) -> rule9)) -> rule6)) -> rule2))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple7 triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple5 ((triple7 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple4) -> (rule3 % int3)) ((triple4 ((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((triple4 ((triple4) -> (rule3 % int4))) -> (rule5 % int3)) ((((triple4) -> (rule3 % int4)) ((triple4 ((triple4) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple4) -> (rule3 % int5)) ((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule6 % int2)) triple4) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
((((triple4) -> (rule3 % int5)) ((((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple4) -> (rule3 % int5)) ((triple4 ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5