Bob is rough. Charlie is green. Charlie is not kind. Charlie is not rough. Charlie is round. Gary is big. Gary is not cold. Gary is quiet. Harry is kind. Harry is not rough. Rough people are cold. Round, rough people are green. If someone is kind then they are green. All green, cold people are round. If someone is cold then they are kind. Quiet, big people are kind.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Round, rough people are green.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All green, cold people are round.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Quiet, big people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Harry is not rough.
True
1
proof
[(triple10)]
("Harry" "is" "rough" "-")
triple10
Charlie is kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Harry is green.
True
2
proof
[(((triple9) -> rule3))]
("Harry" "is" "green" "+")
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple9) -> rule3))]
("Harry" "is" "green" "-")
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Gary is not green.
False
4
inv-proof
[(((((triple8 triple6) -> rule6)) -> rule3))]
("Gary" "is" "green" "-")
((((triple8 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Bob is green.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Harry is round.
Unknown
rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Harry" "is" "round" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is rough.[(triple1)] Charlie is green.[(triple2)] Charlie is not kind.[(triple3)] Charlie is not rough.[(triple4)] Charlie is round.[(triple5)] Gary is big.[(triple6)] Gary is not cold.[(triple7)] Gary is quiet.[(triple8)] Harry is kind.[(triple9)] Harry is not rough.[(triple10)] @1: Bob is cold.[(((triple1) -> rule1))] Gary is kind.[(((triple8 triple6) -> rule6))] Harry is green.[(((triple9) -> rule3))] @2: Bob is kind.[(((((triple1) -> rule1)) -> rule5))] Gary is green.[(((((triple8 triple6) -> rule6)) -> rule3))] @3: Bob is green.[(((((((triple1) -> rule1)) -> rule5)) -> rule3))] @4: Bob is round.[(((((((((triple1) -> rule1)) -> rule5)) -> rule3) ((triple1) -> rule1)) -> rule4))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is not cold.
("Gary" "is" "cold" "-")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is not rough.
("Harry" "is" "rough" "-")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple8 triple6) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple8 triple6) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((triple1) -> (rule1 % int4))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4