Anne is rough. Anne is smart. Bob is nice. Bob is smart. Gary is nice. Gary is red. Gary is not rough. Gary is smart. Gary is young. Harry is rough. If Harry is cold then Harry is not young. If someone is rough then they are cold. If someone is white then they are not smart. If someone is cold and not young then they are smart. If someone is nice and smart then they are red. If someone is red then they are nice. Smart people are nice.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is cold then Harry is not young.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "young" "-"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are not smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "-"))
If someone is cold and not young then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "smart" "+"))
If someone is nice and smart then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Gary is not rough.
True
1
proof
[(triple7)]
("Gary" "is" "rough" "-")
triple7
Bob is not nice.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule7))]
("Bob" "is" "nice" "-")
triple3
((triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
True
3
proof
[(((triple3 triple4) -> rule5) OR ((((triple4) -> rule7) triple4) -> rule5))]
("Bob" "is" "red" "+")
((triple3 triple4) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple4) -> (rule7 % int2)) triple4) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is not cold.
False
2
inv-proof
[(((triple10) -> rule2))]
("Harry" "is" "cold" "-")
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not young.
True
3
proof
[(((((triple10) -> rule2)) -> rule1))]
("Harry" "is" "young" "-")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule1))]
("Harry" "is" "young" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
True
6
proof
[(((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4))]
("Harry" "is" "smart" "+")
((((triple10) -> (rule2 % int3)) ((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not smart.
False
6
inv-proof
[(((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4))]
("Harry" "is" "smart" "-")
((((triple10) -> (rule2 % int3)) ((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
True
7
proof
[(((((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule7))]
("Harry" "is" "nice" "+")
((((((triple10) -> (rule2 % int4)) ((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is not nice.
False
7
inv-proof
[(((((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule7))]
("Harry" "is" "nice" "-")
((((((triple10) -> (rule2 % int4)) ((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is red.
True
14
proof
[(((((((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule7) ((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule5))]
("Harry" "is" "red" "+")
((((((((triple10) -> (rule2 % int5)) ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple10) -> (rule2 % int5)) ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not young.
("Harry" "is" "young" "-")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Harry is not red.
False
14
inv-proof
[(((((((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule7) ((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule5))]
("Harry" "is" "red" "-")
((((((((triple10) -> (rule2 % int5)) ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple10) -> (rule2 % int5)) ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not young.
("Harry" "is" "young" "-")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "cold" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is rough.[(triple1)] Anne is smart.[(triple2)] Bob is nice.[(triple3 OR ((triple4) -> rule7))] Bob is smart.[(triple4)] Gary is nice.[(triple5 OR ((triple6) -> rule6) OR ((triple8) -> rule7))] Gary is not rough.[(triple7)] Gary is red.[(triple6 OR ((triple5 triple8) -> rule5) OR ((((triple8) -> rule7) triple8) -> rule5))] Gary is smart.[(triple8)] Gary is young.[(triple9)] Harry is rough.[(triple10)] @1: Anne is cold.[(((triple1) -> rule2))] Anne is nice.[(((triple2) -> rule7))] Bob is red.[(((triple3 triple4) -> rule5) OR ((((triple4) -> rule7) triple4) -> rule5))] Harry is cold.[(((triple10) -> rule2))] @2: Anne is red.[(((((triple2) -> rule7) triple2) -> rule5))] Harry is not young.[(((((triple10) -> rule2)) -> rule1))] @3: Harry is smart.[(((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4))] @4: Harry is nice.[(((((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule7))] @5: Harry is red.[(((((((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule7) ((((triple10) -> rule2) ((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
((triple6) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple8) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple5 triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8) -> (rule7 % int2)) triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple8
Gary is young.
("Gary" "is" "young" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple3 triple4) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple4) -> (rule7 % int2)) triple4) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple2) -> (rule7 % int2)) triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple10) -> (rule2 % int3)) ((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple10) -> (rule2 % int4)) ((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
((((((((triple10) -> (rule2 % int5)) ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple10) -> (rule2 % int5)) ((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not young.
("Harry" "is" "young" "-")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5