Bob is big. Bob is blue. Bob is kind. Bob is quiet. Bob is round. Charlie is white. Erin is big. Erin is blue. Erin is quiet. Erin is round. Erin is young. Fiona is quiet. Quiet things are white. All young things are quiet. All round, quiet things are kind. If Bob is kind then Bob is round. White, round things are big. All big, quiet things are round. If Erin is white then Erin is blue. All young things are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All round, quiet things are kind.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Bob is kind then Bob is round.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "round" "+"))
White, round things are big.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All big, quiet things are round.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Erin is white then Erin is blue.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "blue" "+"))
All young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Erin is round.
True
1
proof
[(triple10 OR ((triple7 triple9) -> rule6) OR ((triple7 ((triple11) -> rule2)) -> rule6))]
("Erin" "is" "round" "+")
triple10
((triple7 triple9) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple7 ((triple11) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Bob is not big.
False
1
inv-proof
[(triple1 OR ((((triple4) -> rule1) triple5) -> rule5) OR ((((triple4) -> rule1) ((triple3) -> rule4)) -> rule5))]
("Bob" "is" "big" "-")
triple1
((((triple4) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Bob is big.[(triple1 OR ((((triple4) -> rule1) triple5) -> rule5) OR ((((triple4) -> rule1) ((triple3) -> rule4)) -> rule5))] Bob is blue.[(triple2)] Bob is kind.[(triple3 OR ((triple5 triple4) -> rule3) OR ((((triple1 triple4) -> rule6) triple4) -> rule3))] Bob is quiet.[(triple4)] Bob is round.[(triple5 OR ((triple3) -> rule4) OR ((triple1 triple4) -> rule6))] Charlie is white.[(triple6)] Erin is big.[(triple7 OR ((((triple11) -> rule8) triple10) -> rule5) OR ((((triple9) -> rule1) triple10) -> rule5) OR ((((((triple11) -> rule2)) -> rule1) triple10) -> rule5))] Erin is blue.[(triple8 OR ((((triple11) -> rule8)) -> rule7) OR ((((triple9) -> rule1)) -> rule7) OR ((((((triple11) -> rule2)) -> rule1)) -> rule7))] Erin is quiet.[(triple9 OR ((triple11) -> rule2))] Erin is round.[(triple10 OR ((triple7 triple9) -> rule6) OR ((triple7 ((triple11) -> rule2)) -> rule6))] Erin is young.[(triple11)] Fiona is quiet.[(triple12)] @1: Bob is white.[(((triple4) -> rule1))] Erin is kind.[(((triple10 triple9) -> rule3) OR ((triple10 ((triple11) -> rule2)) -> rule3) OR ((((triple7 triple9) -> rule6) triple9) -> rule3) OR ((((triple7 triple9) -> rule6) ((triple11) -> rule2)) -> rule3) OR ((((triple7 ((triple11) -> rule2)) -> rule6) triple9) -> rule3) OR ((((triple7 ((triple11) -> rule2)) -> rule6) ((triple11) -> rule2)) -> rule3))] Erin is white.[(((triple11) -> rule8) OR ((triple9) -> rule1) OR ((((triple11) -> rule2)) -> rule1))] Fiona is white.[(((triple12) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple4) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple5 triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1 triple4) -> (rule6 % int2)) triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple3) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple1 triple4) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
((((triple11) -> (rule8 % int2)) triple10) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple9) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple11) -> (rule2 % int3))) -> (rule1 % int2)) triple10) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple8
((((triple11) -> (rule8 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple9) -> (rule1 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple11) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple10
((triple7 triple9) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple7 ((triple11) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
Bob is white.
("Bob" "is" "white" "+")
((triple4) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple10 triple9) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple10 ((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple7 triple9) -> (rule6 % int2)) triple9) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple7 triple9) -> (rule6 % int3)) ((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple7 ((triple11) -> (rule2 % int3))) -> (rule6 % int2)) triple9) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple7 ((triple11) -> (rule2 % int3))) -> (rule6 % int2)) ((triple11) -> (rule2 % int3))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple11) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple9) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple12) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1