Anne is red. Bob is big. Bob is blue. Bob is quiet. Bob is red. Bob is smart. Bob is white. Bob is young. Fiona is quiet. Fiona is red. Fiona is white. Fiona is young. If something is blue then it is quiet. If something is smart and young then it is blue. If something is big then it is smart. All quiet things are blue. All blue things are big. Red, white things are young.
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and young then it is blue.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Red, white things are young.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Bob is quiet.
True
1
proof
[(triple4 OR ((triple3) -> rule1) OR ((((triple6 triple8) -> rule2)) -> rule1) OR ((((triple6 ((triple5 triple7) -> rule6)) -> rule2)) -> rule1) OR ((((((triple2) -> rule3) triple8) -> rule2)) -> rule1) OR ((((((triple2) -> rule3) ((triple5 triple7) -> rule6)) -> rule2)) -> rule1))]
("Bob" "is" "quiet" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple6 ((triple5 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3)) triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple2) -> (rule3 % int4)) ((triple5 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Fiona is not white.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "white" "-")
triple11
Fiona is blue.
True
2
proof
[(((triple9) -> rule4))]
("Fiona" "is" "blue" "+")
((triple9) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
2
inv-proof
[(((triple9) -> rule4))]
("Fiona" "is" "blue" "-")
((triple9) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
True
3
proof
[(((((triple9) -> rule4)) -> rule5))]
("Fiona" "is" "big" "+")
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule5))]
("Fiona" "is" "big" "-")
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
True
4
proof
[(((((((triple9) -> rule4)) -> rule5)) -> rule3))]
("Fiona" "is" "smart" "+")
((((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is not smart.
False
4
inv-proof
[(((((((triple9) -> rule4)) -> rule5)) -> rule3))]
("Fiona" "is" "smart" "-")
((((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@5: Anne is smart.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule4 <- rule1 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is big.
Unknown
rconc
[@5: Anne is big.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- rule2 <- rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not blue.
Unknown
inv-rconc
[@4: Anne is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule2 <- rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is red.[(triple1)] Bob is big.[(triple2 OR ((triple3) -> rule5) OR ((((triple4) -> rule4)) -> rule5) OR ((((triple6 triple8) -> rule2)) -> rule5) OR ((((triple6 ((triple5 triple7) -> rule6)) -> rule2)) -> rule5))] Bob is blue.[(triple3 OR ((triple4) -> rule4) OR ((triple6 triple8) -> rule2) OR ((triple6 ((triple5 triple7) -> rule6)) -> rule2) OR ((((triple2) -> rule3) triple8) -> rule2) OR ((((triple2) -> rule3) ((triple5 triple7) -> rule6)) -> rule2))] Bob is quiet.[(triple4 OR ((triple3) -> rule1) OR ((((triple6 triple8) -> rule2)) -> rule1) OR ((((triple6 ((triple5 triple7) -> rule6)) -> rule2)) -> rule1) OR ((((((triple2) -> rule3) triple8) -> rule2)) -> rule1) OR ((((((triple2) -> rule3) ((triple5 triple7) -> rule6)) -> rule2)) -> rule1))] Bob is red.[(triple5)] Bob is smart.[(triple6 OR ((triple2) -> rule3) OR ((((triple3) -> rule5)) -> rule3) OR ((((((triple4) -> rule4)) -> rule5)) -> rule3))] Bob is white.[(triple7)] Bob is young.[(triple8 OR ((triple5 triple7) -> rule6))] Fiona is quiet.[(triple9)] Fiona is red.[(triple10)] Fiona is white.[(triple11)] Fiona is young.[(triple12 OR ((triple10 triple11) -> rule6))] @1: Fiona is blue.[(((triple9) -> rule4))] @2: Fiona is big.[(((((triple9) -> rule4)) -> rule5))] @3: Fiona is smart.[(((((((triple9) -> rule4)) -> rule5)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple6 triple8) -> (rule2 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple6 ((triple5 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
triple3
((triple4) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6 triple8) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6 ((triple5 triple7) -> (rule6 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple2) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple5 triple7) -> (rule6 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6 triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple6 ((triple5 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3)) triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple2) -> (rule3 % int4)) ((triple5 triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
triple8
((triple5 triple7) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
((triple10 triple11) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple9) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple9) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3