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