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