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