Bob is quiet. Bob is red. Bob is white. Charlie is blue. Charlie is nice. Charlie is white. Dave is blue. Erin is big. Erin is red. Erin is white. Nice, white things are blue. Young things are nice. If Bob is big then Bob is quiet. All white things are quiet. Big, red things are nice. Blue, young things are nice. If something is big and nice then it is white. If something is blue then it is big.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Nice, white things are blue.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Bob is big then Bob is quiet.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "quiet" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Big, red things are nice.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Blue, young things are nice.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is big and nice then it is white.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Bob is white.
True
1
proof
[(triple3)]
("Bob" "is" "white" "+")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple4 OR ((triple5 triple6) -> rule1))]
("Charlie" "is" "blue" "-")
triple4
((triple5 triple6) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
True
2
proof
[(((triple6) -> rule4) OR ((((((triple4) -> rule8) triple5) -> rule7)) -> rule4))]
("Charlie" "is" "quiet" "+")
((triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((triple4) -> (rule8 % int3)) triple5) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not quiet.
False
2
inv-proof
[(((triple6) -> rule4) OR ((((((triple4) -> rule8) triple5) -> rule7)) -> rule4))]
("Charlie" "is" "quiet" "-")
((triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((triple4) -> (rule8 % int3)) triple5) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is quiet.[(triple1 OR ((triple3) -> rule4))] Bob is red.[(triple2)] Bob is white.[(triple3)] Charlie is blue.[(triple4 OR ((triple5 triple6) -> rule1))] Charlie is nice.[(triple5)] Charlie is white.[(triple6 OR ((((triple4) -> rule8) triple5) -> rule7))] Dave is blue.[(triple7)] Erin is big.[(triple8)] Erin is red.[(triple9)] Erin is white.[(triple10 OR ((triple8 ((triple8 triple9) -> rule5)) -> rule7))] @1: Charlie is big.[(((triple4) -> rule8) OR ((((triple5 triple6) -> rule1)) -> rule8))] Charlie is quiet.[(((triple6) -> rule4) OR ((((((triple4) -> rule8) triple5) -> rule7)) -> rule4))] Dave is big.[(((triple7) -> rule8))] Erin is nice.[(((triple8 triple9) -> rule5))] Erin is quiet.[(((triple10) -> rule4) OR ((((triple8 ((triple8 triple9) -> rule5)) -> rule7)) -> rule4))] @2: Erin is blue.[(((((triple8 triple9) -> rule5) triple10) -> rule1) OR ((((triple8 triple9) -> rule5) ((triple8 ((triple8 triple9) -> rule5)) -> rule7)) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
((triple3) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
((triple5 triple6) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((((triple4) -> (rule8 % int2)) triple5) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
((triple8 ((triple8 triple9) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple4) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple5 triple6) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((triple4) -> (rule8 % int3)) triple5) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((triple7) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple8 triple9) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple10) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple8 ((triple8 triple9) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((triple8 triple9) -> (rule5 % int2)) triple10) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple8 triple9) -> (rule5 % int3)) ((triple8 ((triple8 triple9) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3