Anne is quiet. Bob is red. Charlie is cold. Fiona is quiet. If someone is red then they are young. Quiet people are young. If Anne is young then Anne is red. If Bob is red and Bob is nice then Bob is quiet. If Fiona is young and Fiona is red then Fiona is quiet. All young, cold people are furry. Quiet people are nice. Red, furry people are big.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Anne is young then Anne is red.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "red" "+"))
If Bob is red and Bob is nice then Bob is quiet.
((("Bob" "is" "red" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "quiet" "+"))
If Fiona is young and Fiona is red then Fiona is quiet.
((("Fiona" "is" "young" "+") ("Fiona" "is" "red" "+")) -> ("Fiona" "is" "quiet" "+"))
All young, cold people are furry.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Red, furry people are big.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "cold" "-")
triple3
Fiona is nice.
True
2
proof
[(((triple4) -> rule7))]
("Fiona" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple4) -> rule2))]
("Fiona" "is" "young" "-")
((triple4) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "big" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Anne" "is" "big" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is quiet.[(triple1)] Bob is red.[(triple2)] Charlie is cold.[(triple3)] Fiona is quiet.[(triple4)] @1: Anne is nice.[(((triple1) -> rule7))] Anne is young.[(((triple1) -> rule2))] Bob is young.[(((triple2) -> rule1))] Fiona is nice.[(((triple4) -> rule7))] Fiona is young.[(((triple4) -> rule2))] @2: Anne is red.[(((((triple1) -> rule2)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple4) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2