Fiona is big. All big, green things are red. If Fiona is red and Fiona is furry then Fiona is young. If Fiona is white then Fiona is blue. All big things are young. If something is red then it is young. If Fiona is white and Fiona is blue then Fiona is furry. If something is young then it is red. If something is red then it is furry.
Fiona is big.
("Fiona" "is" "big" "+")
All big, green things are red.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Fiona is red and Fiona is furry then Fiona is young.
((("Fiona" "is" "red" "+") ("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "young" "+"))
If Fiona is white then Fiona is blue.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "blue" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Fiona is white and Fiona is blue then Fiona is furry.
((("Fiona" "is" "white" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "furry" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Fiona is big.
True
1
proof
[(triple1)]
("Fiona" "is" "big" "+")
triple1
Fiona is not big.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "big" "-")
triple1
Fiona is young.
True
2
proof
[(((triple1) -> rule4))]
("Fiona" "is" "young" "+")
((triple1) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Fiona" "is" "young" "-")
((triple1) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("Fiona" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("Fiona" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
True
4
proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule8))]
("Fiona" "is" "furry" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not furry.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule8))]
("Fiona" "is" "furry" "-")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Fiona is big.[(triple1)] @1: Fiona is young.[(((triple1) -> rule4))] @2: Fiona is red.[(((((triple1) -> rule4)) -> rule7))] @3: Fiona is furry.[(((((((triple1) -> rule4)) -> rule7)) -> rule8))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Fiona is young.
("Fiona" "is" "young" "+")
((triple1) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3