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