Charlie is cold. Charlie is smart. Dave is big. Erin is rough. Erin is round. Erin is smart. Erin is young. Big, young people are rough. If someone is cold then they are young. All rough people are big.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Big, young people are rough.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Charlie is smart.
True
1
proof
[(triple2)]
("Charlie" "is" "smart" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple3)]
("Dave" "is" "big" "-")
triple3
Erin is big.
True
2
proof
[(((triple4) -> rule3))]
("Erin" "is" "big" "+")
((triple4) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple4) -> rule3))]
("Erin" "is" "big" "-")
((triple4) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Charlie is cold.[(triple1)] Charlie is smart.[(triple2)] Dave is big.[(triple3)] Erin is rough.[(triple4)] Erin is round.[(triple5)] Erin is smart.[(triple6)] Erin is young.[(triple7)] @1: Charlie is young.[(((triple1) -> rule2))] Erin is big.[(((triple4) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple4) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1