Dave is kind. Fiona is round. Gary is big. Harry is young. Red people are kind. All big people are round. All round people are young. If someone is young then they are red. If someone is big then they are nice. If someone is young then they are red. All nice, young people are big. All nice, round people are kind.
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All nice, young people are big.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All nice, round people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Gary is not big.
False
1
inv-proof
[(triple3)]
("Gary" "is" "big" "-")
triple3
Fiona is young.
True
2
proof
[(((triple2) -> rule3))]
("Fiona" "is" "young" "+")
((triple2) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple4) -> rule4) OR ((triple4) -> rule6))]
("Harry" "is" "red" "-")
((triple4) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple4) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Dave" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Fiona" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is kind.[(triple1)] Fiona is round.[(triple2)] Gary is big.[(triple3)] Harry is young.[(triple4)] @1: Fiona is young.[(((triple2) -> rule3))] Gary is nice.[(((triple3) -> rule5))] Gary is round.[(((triple3) -> rule2))] Harry is red.[(((triple4) -> rule4) OR ((triple4) -> rule6))] @2: Fiona is red.[(((((triple2) -> rule3)) -> rule4) OR ((((triple2) -> rule3)) -> rule6))] Gary is kind.[(((((triple3) -> rule5) ((triple3) -> rule2)) -> rule8) OR ((((((((triple3) -> rule2)) -> rule3)) -> rule4)) -> rule1) OR ((((((((triple3) -> rule2)) -> rule3)) -> rule6)) -> rule1))] Gary is young.[(((((triple3) -> rule2)) -> rule3))] Harry is kind.[(((((triple4) -> rule4)) -> rule1) OR ((((triple4) -> rule6)) -> rule1))] @3: Fiona is kind.[(((((((triple2) -> rule3)) -> rule4)) -> rule1) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))] Gary is red.[(((((((triple3) -> rule2)) -> rule3)) -> rule4) OR ((((((triple3) -> rule2)) -> rule3)) -> rule6))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Fiona is young.
("Fiona" "is" "young" "+")
((triple2) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple4) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule5 % int3)) ((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((((triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
((((((((triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3