Fiona is furry. Gary is blue. All smart things are blue. If something is round and not red then it is not blue. If something is blue and young then it is furry. If something is red then it is round. Blue things are young. Furry things are smart.
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is blue.
("Gary" "is" "blue" "+")
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is round and not red then it is not blue.
((("something" "is" "round" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "-"))
If something is blue and young then it is furry.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is red then it is round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Gary is blue.
True
1
proof
[(triple2)]
("Gary" "is" "blue" "+")
triple2
Fiona is not furry.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "furry" "-")
triple1
Gary is young.
True
2
proof
[(((triple2) -> rule5))]
("Gary" "is" "young" "+")
((triple2) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple2) -> rule5))]
("Gary" "is" "young" "-")
((triple2) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule3))]
("Gary" "is" "furry" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not furry.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule3))]
("Gary" "is" "furry" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
True
5
proof
[(((((triple2 ((triple2) -> rule5)) -> rule3)) -> rule6))]
("Gary" "is" "smart" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Fiona is not young.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule5))]
("Fiona" "is" "young" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Fiona is furry.[(triple1)] Gary is blue.[(triple2)] @1: Fiona is smart.[(((triple1) -> rule6))] Gary is young.[(((triple2) -> rule5))] @2: Fiona is blue.[(((((triple1) -> rule6)) -> rule1))] Gary is furry.[(((triple2 ((triple2) -> rule5)) -> rule3))] @3: Fiona is young.[(((((((triple1) -> rule6)) -> rule1)) -> rule5))] Gary is smart.[(((((triple2 ((triple2) -> rule5)) -> rule3)) -> rule6))]
Fiona is furry.
("Fiona" "is" "furry" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3