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