Charlie is blue. Charlie is young. Fiona is rough. If Fiona is young then Fiona is cold. If Fiona is furry and Fiona is young then Fiona is cold. If something is rough then it is young. If something is quiet then it is not young. If something is cold then it is not furry. If Charlie is not rough and Charlie is not young then Charlie is furry. If something is furry and blue then it is red. If something is red then it is blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Fiona is young then Fiona is cold.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "cold" "+"))
If Fiona is furry and Fiona is young then Fiona is cold.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "cold" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is quiet then it is not young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "-"))
If something is cold then it is not furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "-"))
If Charlie is not rough and Charlie is not young then Charlie is furry.
((("Charlie" "is" "rough" "~") ("Charlie" "is" "young" "~")) -> ("Charlie" "is" "furry" "+"))
If something is furry and blue then it is red.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Charlie is young.
True
1
proof
[(triple2)]
("Charlie" "is" "young" "+")
triple2
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Fiona is young.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "young" "+")
((triple3) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "young" "-")
((triple3) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Fiona" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Fiona" "is" "cold" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not furry.
True
4
proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule5))]
("Fiona" "is" "furry" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is furry.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule5))]
("Fiona" "is" "furry" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Fiona" "is" "blue" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Charlie" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "red" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is blue.[(triple1)] Charlie is young.[(triple2)] Fiona is rough.[(triple3)] @1: Fiona is young.[(((triple3) -> rule3))] @2: Fiona is cold.[(((((triple3) -> rule3)) -> rule1))] @3: Fiona is not furry.[(((((((triple3) -> rule3)) -> rule1)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not furry.
("Fiona" "is" "furry" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3