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