Charlie is big. Erin is big. Harry is quiet. Cold people are smart. All green, smart people are quiet. If someone is red then they are furry. If someone is big then they are quiet. If someone is big then they are smart. Smart people are red.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All green, smart people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Erin is big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Erin is smart.
True
2
proof
[(((triple2) -> rule5))]
("Erin" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("Erin" "is" "red" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
True
4
proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule3))]
("Erin" "is" "furry" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Charlie is not furry.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule6)) -> rule3))]
("Charlie" "is" "furry" "-")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not furry.
Unknown
inv-rconc
[@3: Harry is furry.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Charlie is big.[(triple1)] Erin is big.[(triple2)] Harry is quiet.[(triple3)] @1: Charlie is quiet.[(((triple1) -> rule4))] Charlie is smart.[(((triple1) -> rule5))] Erin is quiet.[(((triple2) -> rule4))] Erin is smart.[(((triple2) -> rule5))] @2: Charlie is red.[(((((triple1) -> rule5)) -> rule6))] Erin is red.[(((((triple2) -> rule5)) -> rule6))] @3: Charlie is furry.[(((((((triple1) -> rule5)) -> rule6)) -> rule3))] Erin is furry.[(((((((triple2) -> rule5)) -> rule6)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3