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