Bob is cold. Bob is quiet. Bob is young. Dave is cold. Dave is quiet. Dave is red. Dave is not rough. Dave is white. Dave is young. Fiona is big. Fiona is cold. Fiona is not quiet. Fiona is red. Fiona is rough. Fiona is white. Fiona is young. If someone is cold and rough then they are big. White people are big. If Dave is not quiet then Dave is rough. If Fiona is red and Fiona is cold then Fiona is rough. All quiet people are cold. Big, cold people are red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is cold and rough then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If Dave is not quiet then Dave is rough.
((("Dave" "is" "quiet" "~")) -> ("Dave" "is" "rough" "+"))
If Fiona is red and Fiona is cold then Fiona is rough.
((("Fiona" "is" "red" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "rough" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Big, cold people are red.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Fiona is young.
True
1
proof
[(triple16)]
("Fiona" "is" "young" "+")
triple16
Dave is not young.
False
1
inv-proof
[(triple9)]
("Dave" "is" "young" "-")
triple9
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule5))] Bob is quiet.[(triple2)] Bob is young.[(triple3)] Dave is cold.[(triple4 OR ((triple5) -> rule5))] Dave is not rough.[(triple7)] Dave is quiet.[(triple5)] Dave is red.[(triple6 OR ((((triple8) -> rule2) triple4) -> rule6) OR ((((triple8) -> rule2) ((triple5) -> rule5)) -> rule6))] Dave is white.[(triple8)] Dave is young.[(triple9)] Fiona is big.[(triple10 OR ((triple15) -> rule2) OR ((triple11 triple14) -> rule1) OR ((triple11 ((triple13 triple11) -> rule4)) -> rule1))] Fiona is cold.[(triple11)] Fiona is not quiet.[(triple12)] Fiona is red.[(triple13 OR ((triple10 triple11) -> rule6) OR ((((triple15) -> rule2) triple11) -> rule6) OR ((((triple11 triple14) -> rule1) triple11) -> rule6))] Fiona is rough.[(triple14 OR ((triple13 triple11) -> rule4) OR ((((triple10 triple11) -> rule6) triple11) -> rule4) OR ((((((triple15) -> rule2) triple11) -> rule6) triple11) -> rule4))] Fiona is white.[(triple15)] Fiona is young.[(triple16)] @1: Dave is big.[(((triple8) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple5) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
((((triple8) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple8) -> (rule2 % int3)) ((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Fiona is big.
("Fiona" "is" "big" "+")
triple10
((triple15) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple11 triple14) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple11 ((triple13 triple11) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple11
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple12
Fiona is red.
("Fiona" "is" "red" "+")
triple13
((triple10 triple11) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple15) -> (rule2 % int2)) triple11) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple11 triple14) -> (rule1 % int2)) triple11) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple14
((triple13 triple11) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple10 triple11) -> (rule6 % int2)) triple11) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple15) -> (rule2 % int3)) triple11) -> (rule6 % int2)) triple11) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
triple15
Fiona is young.
("Fiona" "is" "young" "+")
triple16
Dave is big.
("Dave" "is" "big" "+")
((triple8) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1