Anne is red. Anne is white. Bob is green. Bob is quiet. Bob is smart. Bob is white. Dave is nice. Dave is quiet. Dave is smart. Fiona is nice. Fiona is quiet. Fiona is not red. Smart, white people are red. All nice, red people are smart. If someone is green then they are quiet. All smart, green people are big. All red people are green. Smart, nice people are green. If someone is quiet and red then they are nice. If Anne is smart and Anne is white then Anne is big.
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Smart, white people are red.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All nice, red people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is green then they are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All smart, green people are big.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Smart, nice people are green.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet and red then they are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Anne is smart and Anne is white then Anne is big.
((("Anne" "is" "smart" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "big" "+"))
Dave is nice.
True
1
proof
[(triple7)]
("Dave" "is" "nice" "+")
triple7
Fiona is not nice.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "nice" "-")
triple10
Bob is red.
True
3
proof
[(((triple5 triple6) -> rule1))]
("Bob" "is" "red" "+")
((triple5 triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not big.
False
3
inv-proof
[(((triple5 triple3) -> rule4) OR ((triple5 ((((triple5 triple6) -> rule1)) -> rule5)) -> rule4) OR ((triple5 ((triple5 ((triple4 ((triple5 triple6) -> rule1)) -> rule7)) -> rule6)) -> rule4))]
("Bob" "is" "big" "-")
((triple5 triple3) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple5 ((((triple5 triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((triple5 ((triple5 ((triple4 ((triple5 triple6) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Anne is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is not big.
False
5
inv-proof
[(((triple9 ((triple9 triple7) -> rule6)) -> rule4))]
("Dave" "is" "big" "-")
((triple9 ((triple9 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is nice.
True
5
proof
[(((((((triple1) -> rule5)) -> rule3) triple1) -> rule7))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not nice.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule3) triple1) -> rule7))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
True
7
proof
[(((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2))]
("Anne" "is" "smart" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is not smart.
False
7
inv-proof
[(((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2))]
("Anne" "is" "smart" "-")
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is big.
True
9
proof
[(((((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2) triple2) -> rule8) OR ((((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2) ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "big" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple1) -> (rule5 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2)) ((triple1) -> (rule5 % int5))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Anne is not big.
False
9
inv-proof
[(((((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2) triple2) -> rule8) OR ((((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2) ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "big" "-")
((((((((((triple1) -> (rule5 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple1) -> (rule5 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2)) ((triple1) -> (rule5 % int5))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "big" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Fiona is green.
Unknown
rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Fiona" "is" "green" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Anne is red.[(triple1)] Anne is white.[(triple2)] Bob is green.[(triple3 OR ((((triple5 triple6) -> rule1)) -> rule5) OR ((triple5 ((triple4 ((triple5 triple6) -> rule1)) -> rule7)) -> rule6))] Bob is quiet.[(triple4 OR ((triple3) -> rule3) OR ((((((triple5 triple6) -> rule1)) -> rule5)) -> rule3))] Bob is smart.[(triple5)] Bob is white.[(triple6)] Dave is nice.[(triple7)] Dave is quiet.[(triple8 OR ((((triple9 triple7) -> rule6)) -> rule3))] Dave is smart.[(triple9)] Fiona is nice.[(triple10)] Fiona is not red.[(triple12)] Fiona is quiet.[(triple11)] @1: Anne is green.[(((triple1) -> rule5))] Bob is big.[(((triple5 triple3) -> rule4) OR ((triple5 ((((triple5 triple6) -> rule1)) -> rule5)) -> rule4) OR ((triple5 ((triple5 ((triple4 ((triple5 triple6) -> rule1)) -> rule7)) -> rule6)) -> rule4))] Bob is red.[(((triple5 triple6) -> rule1))] Dave is green.[(((triple9 triple7) -> rule6))] @2: Anne is quiet.[(((((triple1) -> rule5)) -> rule3))] Bob is nice.[(((triple4 ((triple5 triple6) -> rule1)) -> rule7) OR ((((triple3) -> rule3) ((triple5 triple6) -> rule1)) -> rule7) OR ((((((((triple5 triple6) -> rule1)) -> rule5)) -> rule3) ((triple5 triple6) -> rule1)) -> rule7))] Dave is big.[(((triple9 ((triple9 triple7) -> rule6)) -> rule4))] @3: Anne is nice.[(((((((triple1) -> rule5)) -> rule3) triple1) -> rule7))] @4: Anne is smart.[(((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2))] @5: Anne is big.[(((((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2) triple2) -> rule8) OR ((((((((((triple1) -> rule5)) -> rule3) triple1) -> rule7) triple1) -> rule2) ((triple1) -> rule5)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((((triple5 triple6) -> (rule1 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple5 ((triple4 ((triple5 triple6) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((((triple5 triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((((triple9 triple7) -> (rule6 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is not red.
("Fiona" "is" "red" "-")
triple12
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple5 triple3) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple5 ((((triple5 triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((triple5 ((triple5 ((triple4 ((triple5 triple6) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((triple5 triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple9 triple7) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((triple4 ((triple5 triple6) -> (rule1 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple5 triple6) -> (rule1 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((((triple5 triple6) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((triple5 triple6) -> (rule1 % int4))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
((triple9 ((triple9 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule3 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
((((((((((triple1) -> (rule5 % int5))) -> (rule3 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2)) ((triple1) -> (rule5 % int5))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5