Bob is not nice. Bob is rough. Bob is young. Erin is nice. Erin is quiet. Gary is blue. Gary is rough. Harry is blue. Harry is not cold. Harry is quiet. Harry is red. Harry is young. Quiet things are young. If Gary is not cold then Gary is not quiet. Blue things are quiet. If something is quiet and red then it is blue. If Harry is quiet then Harry is not cold. If something is young and not quiet then it is nice.
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If Gary is not cold then Gary is not quiet.
((("Gary" "is" "cold" "~")) -> ("Gary" "is" "quiet" "-"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and red then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If Harry is quiet then Harry is not cold.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "cold" "-"))
If something is young and not quiet then it is nice.
((("something" "is" "young" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
Harry is not cold.
True
1
proof
[(triple9 OR ((triple10) -> rule5) OR ((((triple8) -> rule3)) -> rule5))]
("Harry" "is" "cold" "-")
triple9
((triple10) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
False
1
inv-proof
[(triple9 OR ((triple10) -> rule5) OR ((((triple8) -> rule3)) -> rule5))]
("Harry" "is" "cold" "+")
triple9
((triple10) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is not nice.[(triple1)] Bob is rough.[(triple2)] Bob is young.[(triple3)] Erin is nice.[(triple4)] Erin is quiet.[(triple5)] Gary is blue.[(triple6)] Gary is rough.[(triple7)] Harry is blue.[(triple8 OR ((triple10 triple11) -> rule4))] Harry is not cold.[(triple9 OR ((triple10) -> rule5) OR ((((triple8) -> rule3)) -> rule5))] Harry is quiet.[(triple10 OR ((triple8) -> rule3))] Harry is red.[(triple11)] Harry is young.[(triple12 OR ((triple10) -> rule1) OR ((((triple8) -> rule3)) -> rule1))] @1: Erin is young.[(((triple5) -> rule1))] Gary is quiet.[(((triple6) -> rule3))] @2: Gary is young.[(((((triple6) -> rule3)) -> rule1))]
Bob is not nice.
("Bob" "is" "nice" "-")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple10 triple11) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
triple9
((triple10) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple8) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple10) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple5) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2