Anne is young. Gary is smart. Harry is quiet. Quiet people are not green. If someone is quiet and not kind then they are not young. All smart people are not big. If Gary is not kind and Gary is not young then Gary is cold. All kind, quiet people are smart. If someone is cold and not green then they are smart. Quiet people are cold. Green, smart people are not cold.
Anne is young.
("Anne" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Quiet people are not green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "-"))
If someone is quiet and not kind then they are not young.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "young" "-"))
All smart people are not big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "-"))
If Gary is not kind and Gary is not young then Gary is cold.
((("Gary" "is" "kind" "~") ("Gary" "is" "young" "~")) -> ("Gary" "is" "cold" "+"))
All kind, quiet people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold and not green then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "smart" "+"))
Quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Green, smart people are not cold.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "-"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Gary is not big.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "big" "-")
((triple2) -> (rule3 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "big" "+")
((triple2) -> (rule3 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Harry is smart.
True
5
proof
[(((((triple3) -> rule7) ((triple3) -> rule1)) -> rule6))]
("Harry" "is" "smart" "+")
((((triple3) -> (rule7 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not smart.
False
5
inv-proof
[(((((triple3) -> rule7) ((triple3) -> rule1)) -> rule6))]
("Harry" "is" "smart" "-")
((((triple3) -> (rule7 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not big.
True
6
proof
[(((((((triple3) -> rule7) ((triple3) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "big" "-")
((((((triple3) -> (rule7 % int4)) ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is big.
False
6
inv-proof
[(((((((triple3) -> rule7) ((triple3) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "big" "+")
((((((triple3) -> (rule7 % int4)) ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "cold" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "cold" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is young.[(triple1)] Gary is smart.[(triple2)] Harry is quiet.[(triple3)] @1: Gary is not big.[(((triple2) -> rule3))] Harry is cold.[(((triple3) -> rule7))] Harry is not green.[(((triple3) -> rule1))] @2: Harry is smart.[(((((triple3) -> rule7) ((triple3) -> rule1)) -> rule6))] @3: Harry is not big.[(((((((triple3) -> rule7) ((triple3) -> rule1)) -> rule6)) -> rule3))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Gary is smart.
("Gary" "is" "smart" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Gary is not big.
("Gary" "is" "big" "-")
((triple2) -> (rule3 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
((triple3) -> (rule1 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule7 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not big.
("Harry" "is" "big" "-")
((((((triple3) -> (rule7 % int4)) ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4