Bob is rough. Fiona is big. Fiona is furry. All rough things are furry. If something is red then it is not white. If Fiona is rough then Fiona is furry. Furry things are red. All white things are red. All red things are big. If something is white then it is not nice. If something is white and not big then it is nice.
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is red then it is not white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "-"))
If Fiona is rough then Fiona is furry.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "furry" "+"))
Furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is white then it is not nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "-"))
If something is white and not big then it is nice.
((("something" "is" "white" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
Fiona is big.
True
1
proof
[(triple2 OR ((((triple3) -> rule4)) -> rule6))]
("Fiona" "is" "big" "+")
triple2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Bob is not rough.
False
1
inv-proof
[(triple1)]
("Bob" "is" "rough" "-")
triple1
Fiona is red.
True
2
proof
[(((triple3) -> rule4))]
("Fiona" "is" "red" "+")
((triple3) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple3) -> rule4))]
("Fiona" "is" "red" "-")
((triple3) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not white.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("Fiona" "is" "white" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is big.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule6))]
("Bob" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not big.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule6))]
("Bob" "is" "big" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "nice" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Bob is rough.[(triple1)] Fiona is big.[(triple2 OR ((((triple3) -> rule4)) -> rule6))] Fiona is furry.[(triple3)] @1: Bob is furry.[(((triple1) -> rule1))] Fiona is red.[(((triple3) -> rule4))] @2: Bob is red.[(((((triple1) -> rule1)) -> rule4))] Fiona is not white.[(((((triple3) -> rule4)) -> rule2))] @3: Bob is big.[(((((((triple1) -> rule1)) -> rule4)) -> rule6))] Bob is not white.[(((((((triple1) -> rule1)) -> rule4)) -> rule2))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Fiona is not white.
("Fiona" "is" "white" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not white.
("Bob" "is" "white" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3