Bob is furry. Bob is red. Bob is rough. Fiona is blue. Fiona is furry. Fiona is red. Fiona is rough. If Bob is red and Bob is blue then Bob is cold. If something is red and young then it is quiet. If Fiona is red and Fiona is blue then Fiona is young. All young, furry things are red. If Bob is furry and Bob is quiet then Bob is cold. If something is red then it is rough. Rough things are blue. If something is young and red then it is rough.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Bob is red and Bob is blue then Bob is cold.
((("Bob" "is" "red" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "cold" "+"))
If something is red and young then it is quiet.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If Fiona is red and Fiona is blue then Fiona is young.
((("Fiona" "is" "red" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "young" "+"))
All young, furry things are red.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Bob is furry and Bob is quiet then Bob is cold.
((("Bob" "is" "furry" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "cold" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is young and red then it is rough.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Bob is rough.
True
1
proof
[(triple3 OR ((triple2) -> rule6))]
("Bob" "is" "rough" "+")
triple3
((triple2) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Fiona is young.
True
3
proof
[(((triple6 triple4) -> rule3) OR ((triple6 ((triple7) -> rule7)) -> rule3) OR ((triple6 ((((triple6) -> rule6)) -> rule7)) -> rule3))]
("Fiona" "is" "young" "+")
((triple6 triple4) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple6 ((triple7) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((triple6 ((((triple6) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not young.
False
3
inv-proof
[(((triple6 triple4) -> rule3) OR ((triple6 ((triple7) -> rule7)) -> rule3) OR ((triple6 ((((triple6) -> rule6)) -> rule7)) -> rule3))]
("Fiona" "is" "young" "-")
((triple6 triple4) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple6 ((triple7) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((triple6 ((((triple6) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Bob is cold.
True
4
proof
[(((triple2 ((triple3) -> rule7)) -> rule1) OR ((triple2 ((((triple2) -> rule6)) -> rule7)) -> rule1))]
("Bob" "is" "cold" "+")
((triple2 ((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not cold.
False
4
inv-proof
[(((triple2 ((triple3) -> rule7)) -> rule1) OR ((triple2 ((((triple2) -> rule6)) -> rule7)) -> rule1))]
("Bob" "is" "cold" "-")
((triple2 ((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is furry.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3 OR ((triple2) -> rule6))] Fiona is blue.[(triple4 OR ((triple7) -> rule7) OR ((((triple6) -> rule6)) -> rule7))] Fiona is furry.[(triple5)] Fiona is red.[(triple6)] Fiona is rough.[(triple7 OR ((triple6) -> rule6) OR ((((triple6 triple4) -> rule3) triple6) -> rule8))] @1: Bob is blue.[(((triple3) -> rule7) OR ((((triple2) -> rule6)) -> rule7))] Fiona is young.[(((triple6 triple4) -> rule3) OR ((triple6 ((triple7) -> rule7)) -> rule3) OR ((triple6 ((((triple6) -> rule6)) -> rule7)) -> rule3))] @2: Bob is cold.[(((triple2 ((triple3) -> rule7)) -> rule1) OR ((triple2 ((((triple2) -> rule6)) -> rule7)) -> rule1))] Fiona is quiet.[(((triple6 ((triple6 triple4) -> rule3)) -> rule2) OR ((triple6 ((triple6 ((triple7) -> rule7)) -> rule3)) -> rule2) OR ((triple6 ((triple6 ((((triple6) -> rule6)) -> rule7)) -> rule3)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple2) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
((triple7) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
((triple6) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple6 triple4) -> (rule3 % int2)) triple6) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((triple6 triple4) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple6 ((triple7) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((triple6 ((((triple6) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((triple2 ((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple6 ((triple6 triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((triple6 ((triple6 ((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((triple6 ((triple6 ((((triple6) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4