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