Dave is big. Dave is cold. Dave is rough. Erin is big. Erin is cold. Erin is rough. Erin is smart. Erin is young. Gary is green. Harry is cold. Harry is green. Harry is red. Harry is rough. Harry is smart. Harry is young. If someone is cold then they are red. If someone is smart and green then they are not big. All red people are young.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is smart and green then they are not big.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "-"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Erin is rough.
True
1
proof
[(triple6)]
("Erin" "is" "rough" "+")
triple6
Harry is not cold.
False
1
inv-proof
[(triple10)]
("Harry" "is" "cold" "-")
triple10
Erin is red.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "red" "+")
((triple5) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Harry is big.
False
3
inv-proof
[(((triple14 triple11) -> rule2))]
("Harry" "is" "big" "+")
((triple14 triple11) -> (rule2 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Dave is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Dave" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Dave" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is rough.[(triple3)] Erin is big.[(triple4)] Erin is cold.[(triple5)] Erin is rough.[(triple6)] Erin is smart.[(triple7)] Erin is young.[(triple8 OR ((((triple5) -> rule1)) -> rule3))] Gary is green.[(triple9)] Harry is cold.[(triple10)] Harry is green.[(triple11)] Harry is red.[(triple12 OR ((triple10) -> rule1))] Harry is rough.[(triple13)] Harry is smart.[(triple14)] Harry is young.[(triple15 OR ((triple12) -> rule3) OR ((((triple10) -> rule1)) -> rule3))] @1: Dave is red.[(((triple2) -> rule1))] Erin is red.[(((triple5) -> rule1))] Harry is not big.[(((triple14 triple11) -> rule2))] @2: Dave is young.[(((((triple2) -> rule1)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple5) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
((triple14 triple11) -> (rule2 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2