Fiona is big. Fiona is kind. Fiona is white. If something is blue and white then it is kind. If something is big then it is white. All kind things are big. Furry, rough things are blue. If something is big then it is quiet. If Fiona is blue and Fiona is white then Fiona is rough.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is blue and white then it is kind.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Furry, rough things are blue.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Fiona is blue and Fiona is white then Fiona is rough.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "rough" "+"))
Fiona is white.
True
1
proof
[(triple3 OR ((triple1) -> rule2) OR ((((triple2) -> rule3)) -> rule2))]
("Fiona" "is" "white" "+")
triple3
((triple1) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not white.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule2) OR ((((triple2) -> rule3)) -> rule2))]
("Fiona" "is" "white" "-")
triple3
((triple1) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
True
2
proof
[(((triple1) -> rule5) OR ((((triple2) -> rule3)) -> rule5))]
("Fiona" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not quiet.
False
2
inv-proof
[(((triple1) -> rule5) OR ((((triple2) -> rule3)) -> rule5))]
("Fiona" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "blue" "+")
@0: Fiona is big.[(triple1 OR ((triple2) -> rule3))] Fiona is kind.[(triple2)] Fiona is white.[(triple3 OR ((triple1) -> rule2) OR ((((triple2) -> rule3)) -> rule2))] @1: Fiona is quiet.[(((triple1) -> rule5) OR ((((triple2) -> rule3)) -> rule5))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
((triple1) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2