Charlie is big. Erin is young. Fiona is rough. If Charlie is young then Charlie is big. All young things are furry. Big things are young.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Charlie is young then Charlie is big.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "big" "+"))
All young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Erin is young.
True
1
proof
[(triple2)]
("Erin" "is" "young" "+")
triple2
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Erin is furry.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "young" "-")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is furry.
Unknown
rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Charlie is big.[(triple1)] Erin is young.[(triple2)] Fiona is rough.[(triple3)] @1: Charlie is young.[(((triple1) -> rule3))] Erin is furry.[(((triple2) -> rule2))] @2: Charlie is furry.[(((((triple1) -> rule3)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2