Bob is big. Bob is cold. Bob is kind. Bob is quiet. Bob is red. Bob is rough. Bob is white. Fiona is big. Fiona is rough. Fiona is white. If Fiona is cold then Fiona is big. If Bob is kind and Bob is rough then Bob is white. If Fiona is cold and Fiona is quiet then Fiona is white. All big, red things are kind. All big things are kind. If something is cold then it is white. If something is cold then it is red. All kind, big things are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Fiona is cold then Fiona is big.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "big" "+"))
If Bob is kind and Bob is rough then Bob is white.
((("Bob" "is" "kind" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "white" "+"))
If Fiona is cold and Fiona is quiet then Fiona is white.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "white" "+"))
All big, red things are kind.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All kind, big things are quiet.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Bob is white.
True
1
proof
[(triple7 OR ((triple2) -> rule6) OR ((triple3 triple6) -> rule2) OR ((((triple1) -> rule5) triple6) -> rule2) OR ((((triple1 triple5) -> rule4) triple6) -> rule2) OR ((((triple1 ((triple2) -> rule7)) -> rule4) triple6) -> rule2))]
("Bob" "is" "white" "+")
triple7
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple3 triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1) -> (rule5 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 ((triple2) -> (rule7 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not white.
False
1
inv-proof
[(triple7 OR ((triple2) -> rule6) OR ((triple3 triple6) -> rule2) OR ((((triple1) -> rule5) triple6) -> rule2) OR ((((triple1 triple5) -> rule4) triple6) -> rule2) OR ((((triple1 ((triple2) -> rule7)) -> rule4) triple6) -> rule2))]
("Bob" "is" "white" "-")
triple7
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple3 triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1) -> (rule5 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 ((triple2) -> (rule7 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Fiona is kind.
True
2
proof
[(((triple8) -> rule5))]
("Fiona" "is" "kind" "+")
((triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple8) -> rule5))]
("Fiona" "is" "kind" "-")
((triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
True
4
proof
[(((((triple8) -> rule5) triple8) -> rule8))]
("Fiona" "is" "quiet" "+")
((((triple8) -> (rule5 % int2)) triple8) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not quiet.
False
4
inv-proof
[(((((triple8) -> rule5) triple8) -> rule8))]
("Fiona" "is" "quiet" "-")
((((triple8) -> (rule5 % int2)) triple8) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3 OR ((triple1) -> rule5) OR ((triple1 triple5) -> rule4) OR ((triple1 ((triple2) -> rule7)) -> rule4))] Bob is quiet.[(triple4 OR ((triple3 triple1) -> rule8) OR ((((triple1) -> rule5) triple1) -> rule8) OR ((((triple1 triple5) -> rule4) triple1) -> rule8) OR ((((triple1 ((triple2) -> rule7)) -> rule4) triple1) -> rule8))] Bob is red.[(triple5 OR ((triple2) -> rule7))] Bob is rough.[(triple6)] Bob is white.[(triple7 OR ((triple2) -> rule6) OR ((triple3 triple6) -> rule2) OR ((((triple1) -> rule5) triple6) -> rule2) OR ((((triple1 triple5) -> rule4) triple6) -> rule2) OR ((((triple1 ((triple2) -> rule7)) -> rule4) triple6) -> rule2))] Fiona is big.[(triple8)] Fiona is rough.[(triple9)] Fiona is white.[(triple10)] @1: Fiona is kind.[(((triple8) -> rule5))] @2: Fiona is quiet.[(((((triple8) -> rule5) triple8) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple1 triple5) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple1 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3 triple1) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 triple5) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 ((triple2) -> (rule7 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple3 triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1) -> (rule5 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1 ((triple2) -> (rule7 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple8) -> (rule5 % int2)) triple8) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2