Charlie is kind. Erin is cold. If someone is white then they are kind. All cold, smart people are young. All cold people are smart. All green people are young. Young people are kind. If someone is young and smart then they are kind.
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All cold, smart people are young.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and smart then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Erin is smart.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "smart" "-")
((triple2) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Erin" "is" "young" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not young.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Erin" "is" "young" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule5) OR ((((triple2 ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule6))]
("Erin" "is" "kind" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not kind.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule5) OR ((((triple2 ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule6))]
("Erin" "is" "kind" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is kind.[(triple1)] Erin is cold.[(triple2)] @1: Erin is smart.[(((triple2) -> rule3))] @2: Erin is young.[(((triple2 ((triple2) -> rule3)) -> rule2))] @3: Erin is kind.[(((((triple2 ((triple2) -> rule3)) -> rule2)) -> rule5) OR ((((triple2 ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule6))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3