Bob is cold. Erin is not blue. Gary is red. Harry is cold. Red people are quiet. If Bob is not smart then Bob is red. Red people are young. If Harry is blue then Harry is not young. If Harry is blue then Harry is not smart. If someone is quiet then they are not nice. If Gary is cold then Gary is smart. If someone is red and not nice then they are not cold.
Bob is cold.
("Bob" "is" "cold" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Gary is red.
("Gary" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is not smart then Bob is red.
((("Bob" "is" "smart" "~")) -> ("Bob" "is" "red" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Harry is blue then Harry is not young.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "young" "-"))
If Harry is blue then Harry is not smart.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "smart" "-"))
If someone is quiet then they are not nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
If Gary is cold then Gary is smart.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "smart" "+"))
If someone is red and not nice then they are not cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "cold" "-"))
Harry is cold.
True
1
proof
[(triple4)]
("Harry" "is" "cold" "+")
triple4
Erin is blue.
False
1
inv-proof
[(triple2)]
("Erin" "is" "blue" "+")
triple2
Gary is quiet.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not nice.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("Gary" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("Gary" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not cold.
True
5
proof
[(((triple3 ((((triple3) -> rule1)) -> rule6)) -> rule8))]
("Gary" "is" "cold" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule6)) -> rule8))]
("Gary" "is" "cold" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "smart" "-")
Bob is young.
Unknown
rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is cold.[(triple1)] Erin is not blue.[(triple2)] Gary is red.[(triple3)] Harry is cold.[(triple4)] @1: Gary is quiet.[(((triple3) -> rule1))] Gary is young.[(((triple3) -> rule3))] @2: Gary is not nice.[(((((triple3) -> rule1)) -> rule6))] @3: Gary is not cold.[(((triple3 ((((triple3) -> rule1)) -> rule6)) -> rule8))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Erin is not blue.
("Erin" "is" "blue" "-")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not cold.
("Gary" "is" "cold" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3