Anne is cold. Anne is furry. Anne is not red. Anne is white. Fiona is furry. Fiona is red. Harry is big. Harry is cold. Harry is furry. Harry is red. Harry is smart. Harry is white. Big people are white. Quiet people are not white. If someone is cold and big then they are white. Quiet people are red. All quiet people are smart. All furry people are big.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is white.
("Anne" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Quiet people are not white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "-"))
If someone is cold and big then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Anne is white.
True
1
proof
[(triple4 OR ((((triple2) -> rule6)) -> rule1) OR ((triple1 ((triple2) -> rule6)) -> rule3))]
("Anne" "is" "white" "+")
triple4
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple1 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Harry is not smart.
False
1
inv-proof
[(triple11)]
("Harry" "is" "smart" "-")
triple11
Anne is big.
True
2
proof
[(((triple2) -> rule6))]
("Anne" "is" "big" "+")
((triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple2) -> rule6))]
("Anne" "is" "big" "-")
((triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is white.
True
3
proof
[(((((triple5) -> rule6)) -> rule1))]
("Fiona" "is" "white" "+")
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not white.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule1))]
("Fiona" "is" "white" "-")
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "smart" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "smart" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is not red.[(triple3)] Anne is white.[(triple4 OR ((((triple2) -> rule6)) -> rule1) OR ((triple1 ((triple2) -> rule6)) -> rule3))] Fiona is furry.[(triple5)] Fiona is red.[(triple6)] Harry is big.[(triple7 OR ((triple9) -> rule6))] Harry is cold.[(triple8)] Harry is furry.[(triple9)] Harry is red.[(triple10)] Harry is smart.[(triple11)] Harry is white.[(triple12 OR ((triple7) -> rule1) OR ((triple8 triple7) -> rule3) OR ((((triple9) -> rule6)) -> rule1) OR ((triple8 ((triple9) -> rule6)) -> rule3))] @1: Anne is big.[(((triple2) -> rule6))] Fiona is big.[(((triple5) -> rule6))] @2: Fiona is white.[(((((triple5) -> rule6)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is not red.
("Anne" "is" "red" "-")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple1 ((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple9) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple7) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple8 ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple5) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2