Charlie is rough. Dave is furry. Dave is rough. Erin is smart. Fiona is furry. Fiona is quiet. Fiona is white. Smart, blue people are rough. All blue people are white. All nice people are smart. If someone is furry then they are nice. Rough, blue people are nice. If someone is quiet then they are blue. If Erin is smart and Erin is white then Erin is nice. Furry, smart people are quiet.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Smart, blue people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Rough, blue people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If Erin is smart and Erin is white then Erin is nice.
((("Erin" "is" "smart" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "nice" "+"))
Furry, smart people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Dave is rough.
True
1
proof
[(triple3 OR ((((((triple2) -> rule4)) -> rule3) ((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule1))]
("Dave" "is" "rough" "+")
triple3
((((((triple2) -> (rule4 % int5))) -> (rule3 % int4)) ((((triple2 ((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not rough.
False
1
inv-proof
[(triple3 OR ((((((triple2) -> rule4)) -> rule3) ((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule1))]
("Dave" "is" "rough" "-")
triple3
((((((triple2) -> (rule4 % int5))) -> (rule3 % int4)) ((((triple2 ((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Fiona is blue.
True
2
proof
[(((triple6) -> rule6) OR ((((triple5 ((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule6))]
("Fiona" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple5 ((((triple5) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is not blue.
False
2
inv-proof
[(((triple6) -> rule6) OR ((((triple5 ((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule6))]
("Fiona" "is" "blue" "-")
((triple6) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple5 ((((triple5) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Dave is smart.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Dave" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule3))]
("Fiona" "is" "smart" "-")
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
True
6
proof
[(((((((triple5) -> rule4)) -> rule3) ((triple6) -> rule6)) -> rule1) OR ((((((triple5) -> rule4)) -> rule3) ((((triple5 ((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule1))]
("Fiona" "is" "rough" "+")
((((((triple5) -> (rule4 % int4))) -> (rule3 % int3)) ((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((((((triple5) -> (rule4 % int5))) -> (rule3 % int4)) ((((triple5 ((((triple5) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Dave is not quiet.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8))]
("Dave" "is" "quiet" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is blue.
True
6
proof
[(((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6))]
("Dave" "is" "blue" "+")
((((triple2 ((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not blue.
False
6
inv-proof
[(((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6))]
("Dave" "is" "blue" "-")
((((triple2 ((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is white.
True
7
proof
[(((((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule2))]
("Dave" "is" "white" "+")
((((((triple2 ((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not white.
False
7
inv-proof
[(((((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule2))]
("Dave" "is" "white" "-")
((((((triple2 ((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Erin" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule8 <- FAIL)]]
("Erin" "is" "rough" "-")
Charlie is smart.
Unknown
rconc
[@4: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- rule8 <- FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not nice.
Unknown
inv-rconc
[@4: Erin is nice.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule6 <- rule8 <- FAIL)]]
("Erin" "is" "nice" "-")
Charlie is nice.
Unknown
rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule8 <- FAIL)]]
("Charlie" "is" "nice" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is rough.[(triple1)] Dave is furry.[(triple2)] Dave is rough.[(triple3 OR ((((((triple2) -> rule4)) -> rule3) ((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule1))] Erin is smart.[(triple4)] Fiona is furry.[(triple5)] Fiona is quiet.[(triple6 OR ((triple5 ((((triple5) -> rule4)) -> rule3)) -> rule8))] Fiona is white.[(triple7 OR ((((triple6) -> rule6)) -> rule2) OR ((((((triple5 ((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule2))] @1: Dave is nice.[(((triple2) -> rule4))] Fiona is blue.[(((triple6) -> rule6) OR ((((triple5 ((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule6))] Fiona is nice.[(((triple5) -> rule4))] @2: Dave is smart.[(((((triple2) -> rule4)) -> rule3))] Fiona is smart.[(((((triple5) -> rule4)) -> rule3))] @3: Dave is quiet.[(((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8))] Fiona is rough.[(((((((triple5) -> rule4)) -> rule3) ((triple6) -> rule6)) -> rule1) OR ((((((triple5) -> rule4)) -> rule3) ((((triple5 ((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule1))] @4: Dave is blue.[(((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6))] @5: Dave is white.[(((((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule8)) -> rule6)) -> rule2))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
((((((triple2) -> (rule4 % int5))) -> (rule3 % int4)) ((((triple2 ((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
((triple5 ((((triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
triple7
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((((triple5 ((((triple5) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple5 ((((triple5) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple5) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple5) -> (rule4 % int4))) -> (rule3 % int3)) ((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((((((triple5) -> (rule4 % int5))) -> (rule3 % int4)) ((((triple5 ((((triple5) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2 ((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((((triple2 ((((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5