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