Charlie is not red. Harry is cold. Harry is white. If someone is cold then they are smart. Smart people are big. All cold people are red. If someone is red and not big then they are white. If someone is red and not rough then they are young. White people are young.
Charlie is not red.
("Charlie" "is" "red" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is red and not big then they are white.
((("someone" "is" "red" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "white" "+"))
If someone is red and not rough then they are young.
((("someone" "is" "red" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "+"))
White people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
Charlie is not red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Harry is not white.
False
1
inv-proof
[(triple3)]
("Harry" "is" "white" "-")
triple3
Harry is young.
True
2
proof
[(((triple3) -> rule6))]
("Harry" "is" "young" "+")
((triple3) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "red" "-")
((triple2) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Harry" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Harry" "is" "big" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is not red.[(triple1)] Harry is cold.[(triple2)] Harry is white.[(triple3)] @1: Harry is red.[(((triple2) -> rule3))] Harry is smart.[(((triple2) -> rule1))] Harry is young.[(((triple3) -> rule6))] @2: Harry is big.[(((((triple2) -> rule1)) -> rule2))]
Charlie is not red.
("Charlie" "is" "red" "-")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
((triple2) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2